diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,42 @@
+# 2.13.0
+
+## Language changes
+
+* Update the implementation of the Prelude function `sortBy` to use
+  a merge sort instead of an insertion sort. This improves the both
+  asymptotic and observed performance on sorting tasks.
+
+## UI improvements
+
+* "Type mismatch" errors now show a context giving more information
+  about the location of the error.   The context is shown when the
+  part of the types match, but then some nested types do not.
+  For example, when mathching `{ a : [8], b : [8] }` with
+  `{ a : [8], b : [16] }` the error will be `8` does not match `16`
+  and the context will be `{ b : [ERROR] _ }` indicating that the
+  error is in the length of the sequence of field `b`.
+
+## Bug fixes
+
+* The What4 backend now properly supports Boolector 3.2.2 or later.
+
+* Make error message locations more precise in some cases (issue #1299).
+
+* Make `:reload` behave as expected after loading a module with `:module`
+  (issue #1313).
+
+* Make `include` paths work as expected when nested within another `include`
+  (issue #1321).
+
+* Fix a panic that occurred when loading dependencies before `include`s are
+  resolved (issue #1330).
+
+* Closed issues #1098, #1280, and #1347.
+
+* Merged pull requests #1233, #1300, #1301, #1302, #1303, #1305, #1306, #1307,
+  #1308, #1311, #1312, #1317, #1319, #1323, #1326, #1331, #1333, #1336, #1337,
+  #1338, #1342, #1346, #1348, and #1349.
+
 # 2.12.0
 
 ## Language changes
@@ -43,7 +82,7 @@
   can be combined into a single line by separating them with `;`,
   which is necessary for stating a signature together with a
   definition, etc.
-  
+
 * There is a new `:set path` REPL option that provides an alternative to
   `CRYPTOLPATH` for controlling where to search for imported modules
   (issue #631).
diff --git a/cryptol.cabal b/cryptol.cabal
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -1,6 +1,6 @@
 Cabal-version:       2.4
 Name:                cryptol
-Version:             2.12.0
+Version:             2.13.0
 Synopsis:            Cryptol: The Language of Cryptography
 Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>.
 License:             BSD-3-Clause
@@ -9,7 +9,7 @@
 Maintainer:          cryptol@galois.com
 Homepage:            http://www.cryptol.net/
 Bug-reports:         https://github.com/GaloisInc/cryptol/issues
-Copyright:           2013-2020 Galois Inc.
+Copyright:           2013-2021 Galois Inc.
 Category:            Language
 Build-type:          Simple
 extra-source-files:  bench/data/*.cry
@@ -26,7 +26,7 @@
   type:     git
   location: https://github.com/GaloisInc/cryptol.git
   -- add a tag on release branches
-  tag:      2.12.0
+  tag:      2.13.0
 
 
 flag static
@@ -40,9 +40,10 @@
 library
   Default-language:
     Haskell2010
-  Build-depends:       base              >= 4.8 && < 5,
+  Build-depends:       base              >= 4.9 && < 5,
+                       arithmoi          >= 0.12,
                        async             >= 2.2 && < 2.3,
-                       base-compat       >= 0.6 && < 0.12,
+                       base-compat       >= 0.6 && < 0.13,
                        bv-sized          >= 1.0 && < 1.1,
                        bytestring        >= 0.10,
                        array             >= 0.4,
@@ -56,7 +57,6 @@
                        ghc-prim,
                        GraphSCC          >= 1.0.4,
                        heredoc           >= 0.2,
-                       integer-gmp       >= 1.0 && < 1.1,
                        libBF             >= 0.6 && < 0.7,
                        MemoTrie          >= 0.6 && < 0.7,
                        monad-control     >= 1.0,
@@ -64,7 +64,7 @@
                        parameterized-utils >= 2.0.2,
                        prettyprinter     >= 1.7.0,
                        process           >= 1.2,
-                       sbv               >= 8.6 && < 8.17,
+                       sbv               >= 8.10 && < 9.1,
                        simple-smt        >= 0.9.7,
                        stm               >= 2.4,
                        strict,
@@ -74,8 +74,13 @@
                        mtl               >= 2.2.1,
                        time              >= 1.6.0.1,
                        panic             >= 0.3,
-                       what4             >= 1.2 && < 1.3
+                       what4             >= 1.3 && < 1.4
 
+  if impl(ghc >= 9.0)
+    build-depends:     ghc-bignum        >= 1.0 && < 1.3
+  else
+    build-depends:     integer-gmp       >= 1.0 && < 1.1
+
   Build-tool-depends:  alex:alex, happy:happy
   hs-source-dirs:      src
 
@@ -201,6 +206,7 @@
   Other-modules:       Cryptol.Parser.LexerUtils,
                        Cryptol.Parser.ParserUtils,
                        Cryptol.Prelude,
+                       GHC.Num.Compat,
                        Paths_cryptol,
                        GitRev
 
diff --git a/cryptol/OptParser.hs b/cryptol/OptParser.hs
--- a/cryptol/OptParser.hs
+++ b/cryptol/OptParser.hs
@@ -9,7 +9,6 @@
 
 module OptParser where
 
-import Data.Monoid (Endo(..))
 import Data.Semigroup
 
 import Prelude ()
diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -915,14 +915,9 @@
  * given update pairs.
  */
 updates : {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
-updates xs0 idxs vals = xss!0
- where
-   xss = [ xs0 ] #
-         [ update xs i b
-         | xs <- xss
-         | i  <- idxs
-         | b  <- vals
-         ]
+updates xs0 idxs vals = foldl upd xs0 (zip idxs vals)
+  where
+    upd xs (i,b) = update xs i b
 
 /**
  * Perform a series of updates to a sequence.  The first argument is
@@ -932,14 +927,9 @@
  * given update pairs.
  */
 updatesEnd : {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
-updatesEnd xs0 idxs vals = xss!0
- where
-   xss = [ xs0 ] #
-         [ updateEnd xs i b
-         | xs  <- xss
-         | i   <- idxs
-         | b   <- vals
-         ]
+updatesEnd xs0 idxs vals = foldl upd xs0 (zip idxs vals)
+  where
+    upd xs (i,b) = updateEnd xs i b
 
 /**
  * Produce a sequence using a generating function.
@@ -964,18 +954,16 @@
  * pair of elements that are equivalent according to the order relation.
  */
 sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
-sortBy le vs =
-  if `n == (0 : Integer) then vs
-  else drop`{1 - min 1 n} (insertBy (vs@0) (sortBy le (drop`{min 1 n} vs)))
+sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = take zs.0
   where
-    insertBy : {k} (fin k) => a -> [k]a -> [k+1]a
-    insertBy x0 ys = xys.0 # [last xs]
-      where
-        xs : [k+1]a
-        xs = [x0] # xys.1
-        xys : [k](a, a)
-        xys = [ if le x y then (x, y) else (y, x) | x <- xs | y <- ys ]
-
+    xs' = if `(n/2)  == 1 then xs else sortBy le xs
+    ys' = if `(n/^2) == 1 then ys else sortBy le ys
+    zs  = [ if i == `(n/2)        then (ys'@j, i  , j+1)
+             | j == `(n/^2)       then (xs'@i, i+1, j  )
+             | le (xs'@i) (ys'@j) then (xs'@i, i+1, j  )
+            else                       (ys'@j, i  , j+1)
+          | (_, i, j) <- [ (undefined, 0, 0) ] # zs
+          ]
 
 // GF_2^n polynomial computations -------------------------------------------
 
@@ -1159,27 +1147,22 @@
 sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
 sum xs = foldl' (+) (fromInteger 0) xs
 
-
 /**
  * Compute the product of the values in the sequence.
  */
 product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
 product xs = foldl' (*) (fromInteger 1) xs
 
-
 /**
  * Scan left is like a foldl that also emits the intermediate values.
  */
-scanl : {n, b, a}  (b -> a -> b) -> b -> [n]a -> [n+1]b
-scanl f acc xs = ys
-  where ys = [acc] # [f a x | a <- ys | x <- xs]
+primitive scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a
 
 /**
  * Scan right is like a foldr that also emits the intermediate values.
  */
-scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
-scanr f acc xs = reverse ys
-  where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
+scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1+n]b
+scanr f acc xs = reverse (scanl (\a b -> f b a) acc (reverse xs))
 
 /**
  * Repeat a value.
@@ -1222,5 +1205,4 @@
  * list of successive function applications.
  */
 iterate : {a} (a -> a) -> a -> [inf]a
-iterate f x = xs
-  where xs = [x] # [ f v | v <- xs ]
+iterate f z = scanl (\x _ -> f x) z (zero:[inf]())
diff --git a/lib/Cryptol/Reference.cry b/lib/Cryptol/Reference.cry
--- a/lib/Cryptol/Reference.cry
+++ b/lib/Cryptol/Reference.cry
@@ -44,3 +44,33 @@
     powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]
 
     zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]
+
+/**
+ * Functional left fold.
+ *
+ * foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
+ *
+ * Reference implementation.
+ */
+foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
+foldl f z bs = last (scanl f z bs)
+
+/**
+ * Scan left is like a foldl that also emits the intermediate values.
+ *
+ * Reference implementation.
+ */
+scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a
+scanl f z bs = as
+  where
+    as = [z] # [ f a b | a <- as | b <- bs ]
+
+/**
+ * Map a function iteratively over a seed value, producing an infinite
+ * list of successive function applications.
+ *
+ * Reference implementation.
+ */
+iterate : {a} (a -> a) -> a -> [inf]a
+iterate f z = xs
+  where xs = [z] # [ f x | x <- xs ]
diff --git a/src/Cryptol/AES.hs b/src/Cryptol/AES.hs
--- a/src/Cryptol/AES.hs
+++ b/src/Cryptol/AES.hs
@@ -294,8 +294,10 @@
 
          subWordRcon :: Word32 -> GF28 -> Word32
          subWordRcon w rc = fromBytes [a `xor` rc, b, c, d]
-            where [a, b, c, d] = map sbox $ toBytes w
-
+            where (a, b, c, d) =
+                    case map sbox $ toBytes w of
+                      [a', b', c', d'] -> (a', b', c', d')
+                      bs -> error $ "Unexpected list length in keyExpansionWords: " ++ show (length bs)
 
 -- | Definition of round-constants, as specified in Section 5.2 of the AES standard.
 --   We only need up to the 11th value for AES-128, and fewer than that for AES-192
diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs
--- a/src/Cryptol/Backend/Concrete.hs
+++ b/src/Cryptol/Backend/Concrete.hs
@@ -40,7 +40,7 @@
 import Data.Ratio
 import Numeric (showIntAtBase)
 import qualified LibBF as FP
-import qualified GHC.Integer.GMP.Internals as Integer
+import qualified GHC.Num.Compat as Integer
 
 import qualified Cryptol.Backend.Arch as Arch
 import qualified Cryptol.Backend.FloatHelpers as FP
@@ -340,11 +340,10 @@
   -- NB: under the precondition that `m` is prime,
   -- the only values for which no inverse exists are
   -- congruent to 0 modulo m.
-  znRecip sym m x
-    | r == 0    = raiseError sym DivideByZero
-    | otherwise = pure r
-   where
-     r = Integer.recipModInteger x m
+  znRecip sym m x =
+    case Integer.integerRecipMod x m of
+      Just r  -> integerLit sym r
+      Nothing -> raiseError sym DivideByZero
 
   znPlus  _ = liftBinIntMod (+)
   znMinus _ = liftBinIntMod (-)
diff --git a/src/Cryptol/Backend/Monad.hs b/src/Cryptol/Backend/Monad.hs
--- a/src/Cryptol/Backend/Monad.hs
+++ b/src/Cryptol/Backend/Monad.hs
@@ -383,13 +383,13 @@
   {-# INLINE fmap #-}
 
 instance Applicative Eval where
-  pure  = return
+  pure  = Ready
   (<*>) = ap
   {-# INLINE pure #-}
   {-# INLINE (<*>) #-}
 
 instance Monad Eval where
-  return = Ready
+  return = pure
   (>>=)  = evalBind
   {-# INLINE return #-}
   {-# INLINE (>>=) #-}
diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs
--- a/src/Cryptol/Backend/SBV.hs
+++ b/src/Cryptol/Backend/SBV.hs
@@ -38,7 +38,7 @@
 import           Data.Bits (bit, complement)
 import           Data.List (foldl')
 
-import qualified GHC.Integer.GMP.Internals as Integer
+import qualified GHC.Num.Compat as Integer
 
 import Data.SBV.Dynamic as SBV
 import qualified Data.SBV.Internals as SBV
@@ -429,8 +429,9 @@
 sModRecip sym m x
   -- If the input is concrete, evaluate the answer
   | Just xi <- svAsInteger x
-  = let r = Integer.recipModInteger xi m
-     in if r == 0 then raiseError sym DivideByZero else integerLit sym r
+  = case Integer.integerRecipMod xi m of
+      Just r  -> integerLit sym r
+      Nothing -> raiseError sym DivideByZero
 
   -- If the input is symbolic, create a new symbolic constant
   -- and assert that it is the desired multiplicitive inverse.
diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs
--- a/src/Cryptol/Backend/What4.hs
+++ b/src/Cryptol/Backend/What4.hs
@@ -28,7 +28,7 @@
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Some
 
-import qualified GHC.Integer.GMP.Internals as Integer
+import qualified GHC.Num.Compat as Integer
 
 import qualified What4.Interface as W4
 import qualified What4.SWord as SW
@@ -341,7 +341,7 @@
   wordMult   sym x y = liftIO (SW.bvMul (w4 sym) x y)
   wordNegate sym x   = liftIO (SW.bvNeg (w4 sym) x)
   wordLg2    sym x   = sLg2 (w4 sym) x
- 
+
   wordShiftLeft   sym x y = w4bvShl (w4 sym) x y
   wordShiftRight  sym x y = w4bvLshr (w4 sym) x y
   wordRotateLeft  sym x y = w4bvRol (w4 sym) x y
@@ -668,8 +668,9 @@
 sModRecip sym m x
   -- If the input is concrete, evaluate the answer
   | Just xi <- W4.asInteger x
-  = let r = Integer.recipModInteger xi m
-     in if r == 0 then raiseError sym DivideByZero else integerLit sym r
+  = case Integer.integerRecipMod xi m of
+      Just r  -> integerLit sym r
+      Nothing -> raiseError sym DivideByZero
 
   -- If the input is symbolic, create a new symbolic constant
   -- and assert that it is the desired multiplicitive inverse.
diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs
--- a/src/Cryptol/Eval.hs
+++ b/src/Cryptol/Eval.hs
@@ -550,7 +550,7 @@
     , leTypes  = mempty
     }
 
-  mappend l r = l <> r
+  mappend = (<>)
 
 toListEnv :: GenEvalEnv sym -> ListEnv sym
 toListEnv e =
@@ -566,7 +566,7 @@
 --   locations.
 evalListEnv :: ListEnv sym -> Integer -> GenEvalEnv sym
 evalListEnv (ListEnv vm st tm) i =
-    let v = fmap (Right . ($i)) vm
+    let v = fmap (Right . ($ i)) vm
      in EvalEnv{ envVars = IntMap.union v st
                , envTypes = tm
                }
@@ -664,7 +664,7 @@
       -- `leVars` elements of the comprehension environment into `leStatic` elements
       -- by selecting out the 0th element.
       Inf -> do
-        let allvars = IntMap.union (fmap (Right . ($0)) (leVars lenv)) (leStatic lenv)
+        let allvars = IntMap.union (fmap (Right . ($ 0)) (leVars lenv)) (leStatic lenv)
         let lenv' = lenv { leVars   = IntMap.empty
                          , leStatic = allvars
                          }
diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs
--- a/src/Cryptol/Eval/Concrete.hs
+++ b/src/Cryptol/Eval/Concrete.hs
@@ -250,9 +250,9 @@
   ]
 
 toProjectivePoint :: Value -> Eval PrimeEC.ProjectivePoint
-toProjectivePoint v = PrimeEC.ProjectivePoint <$> f "x" <*> f "y" <*> f "z"
+toProjectivePoint v = PrimeEC.toProjectivePoint <$> f "x" <*> f "y" <*> f "z"
   where
-   f nm = PrimeEC.integerToBigNat . fromVInteger <$> lookupRecord nm v
+   f nm = fromVInteger <$> lookupRecord nm v
 
 fromProjectivePoint :: PrimeEC.ProjectivePoint -> Eval Value
 fromProjectivePoint (PrimeEC.ProjectivePoint x y z) =
diff --git a/src/Cryptol/Eval/Env.hs b/src/Cryptol/Eval/Env.hs
--- a/src/Cryptol/Eval/Env.hs
+++ b/src/Cryptol/Eval/Env.hs
@@ -48,7 +48,7 @@
     { envVars       = IntMap.empty
     , envTypes      = mempty
     }
-  mappend l r = l <> r
+  mappend = (<>)
 
 ppEnv :: Backend sym => sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
 ppEnv sym opts env = brackets . fsep <$> mapM bind (IntMap.toList (envVars env))
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -21,6 +21,8 @@
 {-# LANGUAGE BangPatterns #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.Eval.Generic where
 
 import qualified Control.Exception as X
@@ -35,7 +37,7 @@
 import Data.Ratio ((%))
 
 import Cryptol.TypeCheck.AST
-import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul)
+import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,nAdd)
 import Cryptol.Backend
 import Cryptol.Backend.Concrete (Concrete(..))
 import Cryptol.Backend.Monad( Eval, evalPanic, EvalError(..), Unsupported(..) )
@@ -1814,6 +1816,40 @@
        go1 f a' bs
 
 
+-- scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a
+scanlV :: forall sym. Backend sym => sym -> Prim sym
+scanlV sym =
+  PNumPoly \n ->
+  PTyPoly  \a ->
+  PTyPoly  \_b ->
+  PFun     \f ->
+  PFun     \z ->
+  PStrict  \v ->
+  PPrim
+    do sm <- case v of
+            VSeq _ m   -> scan n f z m
+            VWord _ wv -> scan n f z (VBit <$> asBitsMap sym wv)
+            VStream m  -> scan n f z m
+            _ -> panic "Cryptol.Eval.Generic.scanlV" ["Expected sequence"]
+       mkSeq sym (nAdd (Nat 1) n) a sm
+
+ where
+  scan :: Nat' ->
+          SEval sym (GenValue sym) ->
+          SEval sym (GenValue sym) ->
+          (SeqMap sym (GenValue sym)) ->
+          SEval sym (SeqMap sym (GenValue sym))
+  scan n f z m =
+    do (result, fill) <- sDeclareHole sym "scanl"
+       fill $ memoMap sym (nAdd (Nat 1) n) $ indexSeqMap $ \i ->
+         if i == 0 then z
+         else
+           do r <- result
+              f'  <- fromVFun sym <$> f
+              f'' <- fromVFun sym <$> f' (lookupSeqMap r (i-1))
+              f'' (lookupSeqMap m (i-1))
+       result
+
 -- Random Values ---------------------------------------------------------------
 
 {-# SPECIALIZE randomV ::
@@ -1830,7 +1866,9 @@
       -- unpack the seed into four Word64s
       let mask64 = 0xFFFFFFFFFFFFFFFF
           unpack s = fromInteger (s .&. mask64) : unpack (s `shiftR` 64)
-          [a, b, c, d] = take 4 (unpack seed)
+          (a, b, c, d) = case take 4 (unpack seed) of
+                           [a', b', c', d'] -> (a', b', c', d')
+                           _ -> error "randomV: impossible (infinite seed is finite)"
       in fst $ gen 100 $ seedTFGen (a, b, c, d)
 
 --------------------------------------------------------------------------------
@@ -2199,6 +2237,9 @@
 
   , ("foldl'"     , {-# SCC "Prelude::foldl'" #-}
                     foldl'V sym)
+
+  , ("scanl"      , {-# SCC "Prelude::scanl" #-}
+                    scanlV sym)
 
   , ("deepseq"    , {-# SCC "Prelude::deepseq" #-}
                     PTyPoly \_a ->
diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs
--- a/src/Cryptol/Eval/Reference.lhs
+++ b/src/Cryptol/Eval/Reference.lhs
@@ -31,7 +31,7 @@
 > import qualified Data.Text as T (pack)
 > import LibBF (BigFloat)
 > import qualified LibBF as FP
-> import qualified GHC.Integer.GMP.Internals as Integer
+> import qualified GHC.Num.Compat as Integer
 >
 > import Cryptol.ModuleSystem.Name (asPrim)
 > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
@@ -259,7 +259,7 @@
 >     { envVars  = mempty
 >     , envTypes = mempty
 >     }
->   mappend l r = l <> r
+>   mappend = (<>)
 >
 > -- | Bind a variable in the evaluation environment.
 > bindVar :: (Name, E Value) -> Env -> Env
@@ -1331,8 +1331,10 @@
 > ratRecip x = pure (recip x)
 >
 > zRecip :: Integer -> Integer -> E Integer
-> zRecip m x = if r == 0 then cryError DivideByZero else pure r
->    where r = Integer.recipModInteger x m
+> zRecip m x =
+>   case Integer.integerRecipMod x m of
+>     Just r  -> pure r
+>     Nothing -> cryError DivideByZero
 >
 > zDiv :: Integer -> Integer -> Integer -> E Integer
 > zDiv m x y = f <$> zRecip m y
@@ -1554,17 +1556,17 @@
 >
 > signedShiftRV :: Value
 > signedShiftRV =
->   VNumPoly $ \(Nat n) -> pure $
+>   VNumPoly $ \n -> pure $
 >   VPoly $ \ix -> pure $
 >   VFun $ \v -> pure $
 >   VFun $ \x ->
 >   do amt <- cryToInteger ix x
->      pure $ generateV (Nat n) $ \i ->
+>      pure $ generateV n $ \i ->
 >        do vs <- fromVList <$> v
 >           if i < amt then
->             indexFront (Nat n) vs 0
+>             indexFront n vs 0
 >           else
->             indexFront (Nat n) vs (i - amt)
+>             indexFront n vs (i - amt)
 
 Indexing
 --------
diff --git a/src/Cryptol/IR/FreeVars.hs b/src/Cryptol/IR/FreeVars.hs
--- a/src/Cryptol/IR/FreeVars.hs
+++ b/src/Cryptol/IR/FreeVars.hs
@@ -32,7 +32,7 @@
                 , tyParams  = Set.empty
                 }
 
-  mappend d1 d2 = d1 <> d2
+  mappend = (<>)
 
   mconcat ds = Deps { valDeps   = Set.unions (map valDeps ds)
                     , tyDeps    = Set.unions (map tyDeps  ds)
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -117,6 +117,7 @@
 
 -- Parsing ---------------------------------------------------------------------
 
+-- | Parse a module and expand includes
 parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName)
 parseModule path = do
   getBytes <- getByteReader
@@ -149,8 +150,26 @@
               }
 
   case P.parseModule cfg txt of
-    Right pm -> let fp = fingerprint bytes
-                in fp `seq` return (fp, pm)
+    Right pm ->
+      do let fp = fingerprint bytes
+         pm1 <- case path of
+                  InFile p ->
+                    do r <- getByteReader
+                       mb <- io (removeIncludesModule r p pm)
+                       case mb of
+                         Right ok -> pure ok
+                         Left err -> noIncludeErrors err
+
+                  {- We don't do "include" resolution for in-memory files
+                     because at the moment the include resolution pass requires
+                     the path to the file to be known---this is used when
+                     looking for other inlcude files.  This could be
+                     generalized, but we can do it once we have a concrete use
+                     case as it would help guide the design. -}
+                  InMem {} -> pure pm
+
+         fp `seq` return (fp, pm1)
+
     Left err -> moduleParseError path err
 
 
@@ -210,7 +229,7 @@
        ("Loading module " ++ pretty (P.thing (P.mName pm)))
 
 
-     (nameEnv,tcmod) <- checkModule isrc path pm
+     (nameEnv,tcmod) <- checkModule isrc pm
      tcm <- optionalInstantiate tcmod
 
      -- extend the eval env, unless a functor.
@@ -387,19 +406,17 @@
                   [ "Unable to find the prelude" ]
 
 -- | Load a module, be it a normal module or a functor instantiation.
-checkModule ::
-  ImportSource -> ModulePath -> P.Module PName ->
-  ModuleM (R.NamingEnv, T.Module)
-checkModule isrc path m =
+checkModule :: ImportSource -> P.Module PName -> ModuleM (R.NamingEnv, T.Module)
+checkModule isrc m =
   case P.mInstance m of
-    Nothing -> checkSingleModule T.tcModule isrc path m
+    Nothing -> checkSingleModule T.tcModule isrc m
     Just fmName ->
       do mbtf <- getLoadedMaybe (thing fmName)
          case mbtf of
            Just tf ->
              do renThis <- io $ newIORef (lmNamingEnv tf)
                 let how = T.tcModuleInst renThis (lmModule tf)
-                (_,m') <- checkSingleModule how isrc path m
+                (_,m') <- checkSingleModule how isrc m
                 newEnv <- io $ readIORef renThis
                 pure (newEnv,m')
            Nothing -> panic "checkModule"
@@ -409,35 +426,21 @@
 -- | Typecheck a single module.  If the module is an instantiation
 -- of a functor, then this just type-checks the instantiating parameters.
 -- See 'checkModule'
+-- Note: we assume that @include@s have already been processed
 checkSingleModule ::
   Act (P.Module Name) T.Module {- ^ how to check -} ->
   ImportSource                 {- ^ why are we loading this -} ->
-  ModulePath                   {- path -} ->
   P.Module PName               {- ^ module to check -} ->
   ModuleM (R.NamingEnv,T.Module)
-checkSingleModule how isrc path m = do
+checkSingleModule how isrc m = do
 
   -- check that the name of the module matches expectations
   let nm = importedModule isrc
   unless (notParamInstModName nm == thing (P.mName m))
          (moduleNameMismatch nm (mName m))
 
-  -- remove includes first; we only do this for actual files.
-  -- it is less clear what should happen for in-memory things, and since
-  -- this is a more-or-less obsolete feature, we are just not doing
-  -- ot for now.
-  e   <- case path of
-           InFile p -> do
-             r <- getByteReader
-             io (removeIncludesModule r p m)
-           InMem {} -> pure (Right m)
-
-  nim <- case e of
-           Right nim  -> return nim
-           Left ierrs -> noIncludeErrors ierrs
-
   -- remove pattern bindings
-  npm <- noPat nim
+  npm <- noPat m
 
   -- rename everything
   renMod <- renameModule npm
diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs
--- a/src/Cryptol/ModuleSystem/Env.hs
+++ b/src/Cryptol/ModuleSystem/Env.hs
@@ -260,8 +260,8 @@
                  Just c -> dynModContext me <> c
                  Nothing -> panic "focusedEnv"
                               [ "Focused modules not loaded: " ++ show (pp fm) ]
-  
 
+
 -- Loaded Modules --------------------------------------------------------------
 
 -- | The location of a module
@@ -318,7 +318,7 @@
   mempty = LoadedModules { lmLoadedModules = []
                          , lmLoadedParamModules = []
                          }
-  mappend l r = l <> r
+  mappend = (<>)
 
 data LoadedModule = LoadedModule
   { lmName              :: ModName
@@ -419,7 +419,7 @@
     , deTySyns = mempty
     , deEnv    = mempty
     }
-  mappend de1 de2 = de1 <> de2
+  mappend = (<>)
 
 -- | Build 'IfaceDecls' that correspond to all of the bindings in the
 -- dynamic environment.
diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs
--- a/src/Cryptol/ModuleSystem/Interface.hs
+++ b/src/Cryptol/ModuleSystem/Interface.hs
@@ -146,7 +146,7 @@
 
 instance Monoid IfaceDecls where
   mempty      = IfaceDecls Map.empty Map.empty Map.empty Map.empty Map.empty
-  mappend l r = l <> r
+  mappend     = (<>)
   mconcat ds  = IfaceDecls
     { ifTySyns   = Map.unions (map ifTySyns   ds)
     , ifNewtypes = Map.unions (map ifNewtypes ds)
diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs
--- a/src/Cryptol/ModuleSystem/Monad.hs
+++ b/src/Cryptol/ModuleSystem/Monad.hs
@@ -339,7 +339,7 @@
 
 instance Monad m => Monad (ModuleT m) where
   {-# INLINE return #-}
-  return x      = ModuleT (return x)
+  return        = pure
 
   {-# INLINE (>>=) #-}
   m >>= f       = ModuleT (unModuleT m >>= unModuleT . f)
diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs
--- a/src/Cryptol/ModuleSystem/Name.hs
+++ b/src/Cryptol/ModuleSystem/Name.hs
@@ -10,6 +10,7 @@
 
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -183,12 +184,12 @@
 instance PPName Name where
   ppNameFixity n = nameFixity n
 
-  ppInfixName n @ Name { .. }
+  ppInfixName n@Name { .. }
     | isInfixIdent nIdent = ppName n
     | otherwise           = panic "Name" [ "Non-infix name used infix"
                                          , show nIdent ]
 
-  ppPrefixName n @ Name { .. } = optParens (isInfixIdent nIdent) (ppName n)
+  ppPrefixName n@Name { .. } = optParens (isInfixIdent nIdent) (ppName n)
 
 
 -- | Pretty-print a name with its source location information.
diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs
--- a/src/Cryptol/ModuleSystem/NamingEnv.hs
+++ b/src/Cryptol/ModuleSystem/NamingEnv.hs
@@ -17,6 +17,8 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE OverloadedStrings #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.ModuleSystem.NamingEnv where
 
 import Data.List (nub)
diff --git a/src/Cryptol/ModuleSystem/Renamer/Monad.hs b/src/Cryptol/ModuleSystem/Renamer/Monad.hs
--- a/src/Cryptol/ModuleSystem/Renamer/Monad.hs
+++ b/src/Cryptol/ModuleSystem/Renamer/Monad.hs
@@ -104,7 +104,7 @@
 
 instance Monad RenameM where
   {-# INLINE return #-}
-  return x      = RenameM (return x)
+  return        = pure
 
   {-# INLINE (>>=) #-}
   m >>= k       = RenameM (unRenameM m >>= unRenameM . k)
diff --git a/src/Cryptol/Parser/Layout.hs b/src/Cryptol/Parser/Layout.hs
--- a/src/Cryptol/Parser/Layout.hs
+++ b/src/Cryptol/Parser/Layout.hs
@@ -36,7 +36,7 @@
 
     - The implicit layout block is ended by:
           * a token than is less indented that the block, or
-          * `)`, `}`, `]`, or 
+          * `)`, `}`, `]`, or
           * ',' but only if there is an outer paren block
           block's column.
     - When an implicit layout block ends, we insert a "virtual end block"
@@ -141,7 +141,9 @@
       curTok : go stack lastVirt False advanceTokens
 
     where
-    curTok : advanceTokens = tokens
+    (curTok, advanceTokens) = case tokens of
+                                (curTok' : advanceTokens') -> (curTok', advanceTokens')
+                                [] -> error "layout: Unexpected empty list of tokens"
     curTokTy               = tokenType (thing curTok)
     curRange               = srcRange curTok
     curLoc                 = from curRange
diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs
--- a/src/Cryptol/Parser/NoInclude.hs
+++ b/src/Cryptol/Parser/NoInclude.hs
@@ -116,11 +116,11 @@
   fmap = liftM
 
 instance A.Applicative NoIncM where
-  pure = return
+  pure x = M (pure x)
   (<*>) = ap
 
 instance Monad NoIncM where
-  return x = M (return x)
+  return   = pure
   m >>= f  = M (unM m >>= unM . f)
 
 instance Fail.MonadFail NoIncM where
@@ -196,7 +196,9 @@
   case parseProgramWith (defaultConfig { cfgSource = thing lf, cfgPreProc = guessPreProc (thing lf) }) source of
 
     Right prog -> do
-      Program ds <- withIncPath (thing lf) (noIncludeProgram prog)
+      Program ds <-
+        do path <- fromIncPath (thing lf)
+           withIncPath path (noIncludeProgram prog)
       return ds
 
     Left err -> M (raise [IncludeParseError err])
diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs
--- a/src/Cryptol/Parser/NoPat.hs
+++ b/src/Cryptol/Parser/NoPat.hs
@@ -565,9 +565,11 @@
               deriving (Show,Generic, NFData)
 
 instance Functor NoPatM where fmap = liftM
-instance Applicative NoPatM where pure = return; (<*>) = ap
+instance Applicative NoPatM where
+  pure x = M (pure x)
+  (<*>) = ap
 instance Monad NoPatM where
-  return x  = M (return x)
+  return    = pure
   M x >>= k = M (x >>= unM . k)
 
 -- | Pick a new name, to be used when desugaring patterns.
diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs
--- a/src/Cryptol/Parser/ParserUtils.hs
+++ b/src/Cryptol/Parser/ParserUtils.hs
@@ -13,6 +13,8 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE OverloadedStrings #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.Parser.ParserUtils where
 
 import Data.Maybe(fromMaybe)
@@ -151,11 +153,11 @@
   fmap = liftM
 
 instance Applicative ParseM where
-  pure  = return
+  pure a = P (\_ _ s -> Right (a,s))
   (<*>) = ap
 
 instance Monad ParseM where
-  return a  = P (\_ _ s -> Right (a,s))
+  return    = pure
   m >>= k   = P (\cfg p s1 -> case unP m cfg p s1 of
                             Left e       -> Left e
                             Right (a,s2) -> unP (k a) cfg p s2)
@@ -382,7 +384,7 @@
 eFromToBy r e1 e2 e3 isStrictBound =
   case (asETyped e1, asETyped e2, asETyped e3) of
     (Just (e1', t), Nothing, Nothing) -> eFromToByTyped r e1' e2 e3 (Just t) isStrictBound
-    (Nothing, Just (e2', t), Nothing) -> eFromToByTyped r e1 e2' e3 (Just t) isStrictBound   
+    (Nothing, Just (e2', t), Nothing) -> eFromToByTyped r e1 e2' e3 (Just t) isStrictBound
     (Nothing, Nothing, Just (e3', t)) -> eFromToByTyped r e1 e2 e3' (Just t) isStrictBound
     (Nothing, Nothing, Nothing)       -> eFromToByTyped r e1 e2 e3 Nothing isStrictBound
     _ -> errorMessage r ["A sequence enumeration may have at most one element type annotation."]
@@ -400,7 +402,7 @@
 eFromToDownBy r e1 e2 e3 isStrictBound =
   case (asETyped e1, asETyped e2, asETyped e3) of
     (Just (e1', t), Nothing, Nothing) -> eFromToDownByTyped r e1' e2 e3 (Just t) isStrictBound
-    (Nothing, Just (e2', t), Nothing) -> eFromToDownByTyped r e1 e2' e3 (Just t) isStrictBound   
+    (Nothing, Just (e2', t), Nothing) -> eFromToDownByTyped r e1 e2' e3 (Just t) isStrictBound
     (Nothing, Nothing, Just (e3', t)) -> eFromToDownByTyped r e1 e2 e3' (Just t) isStrictBound
     (Nothing, Nothing, Nothing)       -> eFromToDownByTyped r e1 e2 e3 Nothing isStrictBound
     _ -> errorMessage r ["A sequence enumeration may have at most one element type annotation."]
@@ -575,7 +577,8 @@
 
 -- NOTE: The list of patterns is reversed!
 mkProperty :: LPName -> [Pattern PName] -> Expr PName -> Decl PName
-mkProperty f ps e = DBind Bind { bName       = f
+mkProperty f ps e = at (f,e) $
+                    DBind Bind { bName       = f
                                , bParams     = reverse ps
                                , bDef        = at e (Located emptyRange (DExpr e))
                                , bSignature  = Nothing
diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs
--- a/src/Cryptol/PrimeEC.hs
+++ b/src/Cryptol/PrimeEC.hs
@@ -18,16 +18,27 @@
 -- in order to speed up the basic modular arithmetic operations.
 -----------------------------------------------------------------------------
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE UnboxedTuples #-}
 
+#if __GLASGOW_HASKELL__ >= 900
+-- On GHC 9.0 or later—that is, when building with ghc-bignum—BigNum# is an
+-- unlifted type, so we need UnliftedNewtypes to declare a newtype on top of
+-- it. On older versions of GHC, BigNat# is simply a synonym for BigNat. BigNat
+-- is lifted, so declaring a newtype on top of it works out of the box.
+{-# LANGUAGE UnliftedNewtypes #-}
+#endif
+
 module Cryptol.PrimeEC
   ( PrimeModulus
   , primeModulus
   , ProjectivePoint(..)
-  , integerToBigNat
-  , Integer.bigNatToInteger
+  , toProjectivePoint
+  , BN.integerToBigNat
+  , BN.bigNatToInteger
 
   , ec_double
   , ec_add_nonzero
@@ -36,10 +47,9 @@
   ) where
 
 
-import           GHC.Integer.GMP.Internals (BigNat)
-import qualified GHC.Integer.GMP.Internals as Integer
-import           GHC.Prim
-import           Data.Bits
+import           GHC.Num.Compat (BigNat#)
+import qualified GHC.Num.Compat as BN
+import           GHC.Exts
 
 import Cryptol.TypeCheck.Solver.InfNat (widthInteger)
 import Cryptol.Utils.Panic
@@ -48,173 +58,103 @@
 --   homogenous coordinates.
 data ProjectivePoint =
   ProjectivePoint
-  { px :: !BigNat
-  , py :: !BigNat
-  , pz :: !BigNat
+  { px :: !BigNat#
+  , py :: !BigNat#
+  , pz :: !BigNat#
   }
 
+
+toProjectivePoint :: Integer -> Integer -> Integer -> ProjectivePoint
+toProjectivePoint x y z =
+  ProjectivePoint (BN.integerToBigNat x) (BN.integerToBigNat y) (BN.integerToBigNat z)
+
 -- | The projective "point at infinity", which represents the zero element
 --   of the ECC group.
 zro :: ProjectivePoint
-zro = ProjectivePoint Integer.oneBigNat Integer.oneBigNat Integer.zeroBigNat
-
--- | Coerce an integer value to a @BigNat@.  This operation only really makes
---   sense for nonnegative values, but this condition is not checked.
-integerToBigNat :: Integer -> BigNat
-integerToBigNat (Integer.S# i)  = Integer.wordToBigNat (int2Word# i)
-integerToBigNat (Integer.Jp# b) = b
-integerToBigNat (Integer.Jn# b) = b
+zro = ProjectivePoint (BN.oneBigNat (# #)) (BN.oneBigNat (# #)) (BN.zeroBigNat (# #))
 
 -- | Simple newtype wrapping the @BigNat@ value of the
 --   modulus of the underlying field Z p.  This modulus
 --   is required to be prime.
-newtype PrimeModulus = PrimeModulus { primeMod :: BigNat }
+newtype PrimeModulus = PrimeModulus { primeMod :: BigNat# }
 
 
 -- | Inject an integer value into the @PrimeModulus@ type.
 --   This modulus is required to be prime.
 primeModulus :: Integer -> PrimeModulus
-primeModulus = PrimeModulus . integerToBigNat
+primeModulus x = PrimeModulus (BN.integerToBigNat x)
 {-# INLINE primeModulus #-}
 
 
--- Barrett reduction replaces a division by the modulus with
--- two multiplications and some shifting, masking, and additions
--- (and some fairly negligible pre-processing). For the size of
--- moduli we are working with for ECC, this does not appear to be
--- a performance win.  Even for largest NIST curve (P-521) Barrett
--- reduction is about 20% slower than naive modular reduction.
--- Smaller curves are worse WRT the baseline.
-
--- {-# INLINE primeModulus #-}
--- primeModulus :: Integer -> PrimeModulus
--- primeModulus = untrie modulusParameters
-
--- data PrimeModulus = PrimeModulus
---   { primeMod :: !Integer
---   , barrettInverse :: !Integer
---   , barrettK       :: !Int
---   , barrettMask    :: !Integer
---   }
---  deriving (Show, Eq)
-
--- {-# NOINLINE modulusParameters #-}
--- modulusParameters :: Integer :->: PrimeModulus
--- modulusParameters = trie computeModulusParameters
-
--- computeModulusParameters :: Integer -> PrimeModulus
--- computeModulusParameters p = PrimeModulus p inv k mask
---   where
---   k = fromInteger w
-
---   b :: Integer
---   b = 2 ^ (64::Int)
-
---   -- w is the number of 64-bit words required to express p
---   w = (widthInteger p + 63) `div` 64
-
---   mask = b^(k+1) - 1
-
---   -- inv = floor ( b^(2*k) / p )
---   inv = b^(2*k) `div` p
-
--- barrettReduction :: PrimeModulus -> Integer -> Integer
--- barrettReduction p x = go r3
---   where
---     m    = primeMod p
---     k    = barrettK p
---     inv  = barrettInverse p
---     mask = barrettMask p
-
---     -- q1 <- floor (x / b^(k-1))
---     q1 = x `shiftR` (64 * (k-1))
-
---     -- q2 <- q1 * floor ( b^(2*k) / m )
---     q2 = q1 * inv
-
---     -- q3 <- floor (q2 / b^(k+1))
---     q3 = q2 `shiftR` (64 * (k+1))
-
---     -- r1 <- x mod b^(k+1)
---     r1 = x .&. mask
-
---     -- r2 <- (q3 * m) mod b^(k+1)
---     r2 = (q3 * m) .&. mask
-
---     -- r3 <- r1 - r2
---     r3 = r1 - r2
-
---     -- up to 2 multiples of m must be removed
---     go z = if z > m then go (z - m) else z
-
 -- | Modular addition of two values.  The inputs are
 --   required to be in reduced form, and will output
 --   a value in reduced form.
-mod_add :: PrimeModulus -> BigNat -> BigNat -> BigNat
-mod_add p !x !y =
-    case Integer.isNullBigNat# rmp of
-      0# -> rmp
-      _  -> r
-  where r = Integer.plusBigNat x y
-        rmp = Integer.minusBigNat r (primeMod p)
+mod_add :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#
+mod_add p x y =
+  let r = BN.bigNatAdd x y in
+  case BN.bigNatSub r (primeMod p) of
+    (# (# #) | #) -> r
+    (# | rmp #)   -> rmp
 
 -- | Compute the "half" value of a modular integer.  For a given input @x@
 --   this is a value @y@ such that @y+y == x@.  Such values must exist
 --   in @Z p@ when @p > 2@.  The input @x@ is required to be in reduced form,
 --   and will output a value in reduced form.
-mod_half :: PrimeModulus -> BigNat -> BigNat
-mod_half p !x = if Integer.testBitBigNat x 0# then qodd else qeven
+mod_half :: PrimeModulus -> BigNat# -> BigNat#
+mod_half p x = if BN.testBitBigNat x 0# then qodd else qeven
   where
-  qodd  = (Integer.plusBigNat x (primeMod p)) `Integer.shiftRBigNat` 1#
-  qeven = x `Integer.shiftRBigNat` 1#
+  qodd  = (BN.bigNatAdd x (primeMod p)) `BN.shiftRBigNat` 1#
+  qeven = x `BN.shiftRBigNat` 1#
 
 -- | Compute the modular multiplication of two input values.  Currently, this
 --   uses naive modular reduction, and does not require the inputs to be in
 --   reduced form.  The output is in reduced form.
-mod_mul :: PrimeModulus -> BigNat -> BigNat -> BigNat
-mod_mul p !x !y = (Integer.timesBigNat x y) `Integer.remBigNat` (primeMod p)
+mod_mul :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#
+mod_mul p x y = (BN.bigNatMul x y) `BN.bigNatRem` (primeMod p)
 
 -- | Compute the modular difference of two input values.  The inputs are
 --   required to be in reduced form, and will output a value in reduced form.
-mod_sub :: PrimeModulus -> BigNat -> BigNat -> BigNat
-mod_sub p !x !y = mod_add p x (Integer.minusBigNat (primeMod p) y)
+mod_sub :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#
+mod_sub p x y =
+  case BN.bigNatSub (primeMod p) y of
+    (# | y' #) -> mod_add p x y'
+    (# (# #) | #) -> x -- BOGUS!
 
 -- | Compute the modular square of an input value @x@; that is, @x*x@.
 --   The input is not required to be in reduced form, and the output
 --   will be in reduced form.
-mod_square :: PrimeModulus -> BigNat -> BigNat
-mod_square p !x = Integer.sqrBigNat x `Integer.remBigNat` primeMod p
+mod_square :: PrimeModulus -> BigNat# -> BigNat#
+mod_square p x = BN.bigNatSqr x `BN.bigNatRem` primeMod p
 
 -- | Compute the modular scalar multiplication @2x = x+x@.
 --   The input is required to be in reduced form and the output
 --   will be in reduced form.
-mul2 :: PrimeModulus -> BigNat -> BigNat
-mul2 p !x =
-    case Integer.isNullBigNat# rmp of
-      0# -> rmp
-      _  -> r
- where
-   r = x `Integer.shiftLBigNat` 1#
-   rmp = Integer.minusBigNat r (primeMod p)
+mul2 :: PrimeModulus -> BigNat# -> BigNat#
+mul2 p x =
+  let r = x `BN.shiftLBigNat` 1# in
+  case BN.bigNatSub r (primeMod p) of
+    (# (# #) | #) -> r
+    (# | rmp #)   -> rmp
 
 -- | Compute the modular scalar multiplication @3x = x+x+x@.
 --   The input is required to be in reduced form and the output
 --   will be in reduced form.
-mul3 :: PrimeModulus -> BigNat -> BigNat
-mul3 p x = mod_add p x $! mul2 p x
+mul3 :: PrimeModulus -> BigNat# -> BigNat#
+mul3 p x = mod_add p x (mul2 p x)
 
 -- | Compute the modular scalar multiplication @4x = x+x+x+x@.
 --   The input is required to be in reduced form and the output
 --   will be in reduced form.
-mul4 :: PrimeModulus -> BigNat -> BigNat
-mul4 p x = mul2 p $! mul2 p x
+mul4 :: PrimeModulus -> BigNat# -> BigNat#
+mul4 p x = mul2 p (mul2 p x)
 
 -- | Compute the modular scalar multiplication @8x = x+x+x+x+x+x+x+x@.
 --   The input is required to be in reduced form and the output
 --   will be in reduced form.
-mul8 :: PrimeModulus -> BigNat -> BigNat
-mul8 p x = mul2 p $! mul4 p x
+mul8 :: PrimeModulus -> BigNat# -> BigNat#
+mul8 p x = mul2 p (mul4 p x)
 
+
 -- | Compute the elliptic curve group doubling operation.
 --   In other words, if @S@ is a projective point on a curve,
 --   this operation computes @S+S@ in the ECC group.
@@ -225,7 +165,7 @@
 --   reflected across the x axis.
 ec_double :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
 ec_double p (ProjectivePoint sx sy sz) =
-    if Integer.isZeroBigNat sz then zro else ProjectivePoint r18 r23 r13
+    if BN.bigNatIsZero sz then zro else ProjectivePoint r18 r23 r13
 
   where
   r7  = mod_square p sz                   {-  7: t4 <- (t3)^2  -}
@@ -250,22 +190,25 @@
 --   case for adding points which might be the identity.
 ec_add :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
 ec_add p s t
-  | Integer.isZeroBigNat (pz s) = t
-  | Integer.isZeroBigNat (pz t) = s
+  | BN.bigNatIsZero (pz s) = t
+  | BN.bigNatIsZero (pz t) = s
   | otherwise = ec_add_nonzero p s t
 {-# INLINE ec_add #-}
 
 
+
 -- | Compute the elliptic curve group subtraction operation, including the special
 --   cases for subtracting points which might be the identity.
 ec_sub :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
 ec_sub p s t = ec_add p s u
-  where u = t{ py = Integer.minusBigNat (primeMod p) (py t) }
+  where u = case BN.bigNatSub (primeMod p) (py t) of
+              (# | y' #)    -> t{ py = y' }
+              (# (# #) | #) -> panic "ec_sub" ["cooridnate not in reduced form!", show (BN.bigNatToInteger (py t))]
 {-# INLINE ec_sub #-}
 
 
 ec_negate :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
-ec_negate p s = s{ py = Integer.minusBigNat (primeMod p) (py s) }
+ec_negate p s = s{ py = BN.bigNatSubUnsafe (primeMod p) (py s) }
 {-# INLINE ec_negate #-}
 
 -- | Compute the elliptic curve group addition operation
@@ -280,8 +223,8 @@
 --   which instead computes a tangent line to @S@ .
 ec_add_nonzero :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
 ec_add_nonzero p s@(ProjectivePoint sx sy sz) (ProjectivePoint tx ty tz) =
-    if Integer.isZeroBigNat r13 then
-      if Integer.isZeroBigNat r14 then
+    if BN.bigNatIsZero r13 then
+      if BN.bigNatIsZero r14 then
         ec_double p s
       else
         zro
@@ -289,7 +232,7 @@
       ProjectivePoint r32 r37 r27
 
   where
-  tNormalized = Integer.eqBigNat tz Integer.oneBigNat
+  tNormalized = BN.bigNatIsOne tz
 
   tz2 = mod_square p tz
   tz3 = mod_mul p tz tz2
@@ -328,17 +271,17 @@
 --   be added many times.
 ec_normalize :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
 ec_normalize p s@(ProjectivePoint x y z)
-  | Integer.eqBigNat z Integer.oneBigNat = s
-  | otherwise = ProjectivePoint x' y' Integer.oneBigNat
+  | BN.bigNatIsOne z = s
+  | otherwise = ProjectivePoint x' y' (BN.oneBigNat (# #))
  where
   m = primeMod p
 
-  l  = Integer.recipModBigNat z m
-  l2 = Integer.sqrBigNat l
-  l3 = Integer.timesBigNat l l2
+  l  = BN.recipModBigNat z m
+  l2 = BN.bigNatSqr l
+  l3 = BN.bigNatMul l l2
 
-  x' = (Integer.timesBigNat x l2) `Integer.remBigNat` m
-  y' = (Integer.timesBigNat y l3) `Integer.remBigNat` m
+  x' = (BN.bigNatMul x l2) `BN.bigNatRem` m
+  y' = (BN.bigNatMul y l3) `BN.bigNatRem` m
 
 
 -- | Given an integer @k@ and a projective point @S@, compute
@@ -348,30 +291,31 @@
 ec_mult p d s
   | d == 0    = zro
   | d == 1    = s
-  | Integer.isZeroBigNat (pz s) = zro
+  | BN.bigNatIsZero (pz s) = zro
   | otherwise =
       case m of
-        0# -> panic "ec_mult" ["modulus too large", show (Integer.bigNatToInteger (primeMod p))]
+        0# -> panic "ec_mult" ["modulus too large", show (BN.bigNatToInteger (primeMod p))]
         _  -> go m zro
 
  where
    s' = ec_normalize p s
    h  = 3*d
 
-   d' = integerToBigNat d
-   h' = integerToBigNat h
+   d' = BN.integerToBigNat d
+   h' = BN.integerToBigNat h
 
    m = case widthInteger h of
-         Integer.S# mint -> mint
+         BN.IS mint -> mint
          _ -> 0#
 
+   go :: Int# -> ProjectivePoint -> ProjectivePoint
    go i !r
      | tagToEnum# (i ==# 0#) = r
      | otherwise = go (i -# 1#) r'
 
     where
-      h_i = Integer.testBitBigNat h' i
-      d_i = Integer.testBitBigNat d' i
+      h_i = BN.testBitBigNat h' i
+      d_i = BN.testBitBigNat d' i
 
       r' = if h_i then
              if d_i then r2 else ec_add p r2 s'
@@ -395,26 +339,26 @@
   (ProjectivePoint, ProjectivePoint, ProjectivePoint, ProjectivePoint)
 normalizeForTwinMult p s t
      -- S == 0 && T == 0
-   | Integer.isZeroBigNat a && Integer.isZeroBigNat b =
+   | BN.bigNatIsZero a && BN.bigNatIsZero b =
         (zro, zro, zro, zro)
 
      -- S == 0 && T != 0
-   | Integer.isZeroBigNat a =
+   | BN.bigNatIsZero a =
         let tnorm = ec_normalize p t
          in (zro, tnorm, tnorm, ec_negate p tnorm)
 
      -- T == 0 && S != 0
-   | Integer.isZeroBigNat b =
+   | BN.bigNatIsZero b =
         let snorm = ec_normalize p s
          in (snorm, zro, snorm, snorm)
 
      -- S+T == 0, both != 0
-   | Integer.isZeroBigNat c =
+   | BN.bigNatIsZero c =
         let snorm = ec_normalize p s
          in (snorm, ec_negate p snorm, zro, ec_double p snorm)
 
      -- S-T == 0, both != 0
-   | Integer.isZeroBigNat d =
+   | BN.bigNatIsZero d =
         let snorm = ec_normalize p s
          in (snorm, snorm, ec_double p snorm, zro)
 
@@ -441,7 +385,7 @@
 
   abcd = mod_mul p a bcd
 
-  e = Integer.recipModBigNat abcd m
+  e = BN.recipModBigNat abcd m
 
   a_inv = mod_mul p e bcd
   b_inv = mod_mul p e acd
@@ -460,11 +404,11 @@
   d_inv2 = mod_square p d_inv
   d_inv3 = mod_mul p d_inv d_inv2
 
-  s'   = ProjectivePoint (mod_mul p (px s) a_inv2) (mod_mul p (py s) a_inv3) Integer.oneBigNat
-  t'   = ProjectivePoint (mod_mul p (px t) b_inv2) (mod_mul p (py t) b_inv3) Integer.oneBigNat
+  s'   = ProjectivePoint (mod_mul p (px s) a_inv2) (mod_mul p (py s) a_inv3) (BN.oneBigNat (# #))
+  t'   = ProjectivePoint (mod_mul p (px t) b_inv2) (mod_mul p (py t) b_inv3) (BN.oneBigNat (# #))
 
-  spt' = ProjectivePoint (mod_mul p (px spt) c_inv2) (mod_mul p (py spt) c_inv3) Integer.oneBigNat
-  smt' = ProjectivePoint (mod_mul p (px smt) d_inv2) (mod_mul p (py smt) d_inv3) Integer.oneBigNat
+  spt' = ProjectivePoint (mod_mul p (px spt) c_inv2) (mod_mul p (py spt) c_inv3) (BN.oneBigNat (# #))
+  smt' = ProjectivePoint (mod_mul p (px smt) d_inv2) (mod_mul p (py smt) d_inv3) (BN.oneBigNat (# #))
 
 
 -- | Given an integer @j@ and a projective point @S@, together with
@@ -477,52 +421,52 @@
   Integer -> ProjectivePoint ->
   Integer -> ProjectivePoint ->
   ProjectivePoint
-ec_twin_mult p (integerToBigNat -> d0) s (integerToBigNat -> d1) t =
+ec_twin_mult p (BN.integerToBigNat -> d0) s (BN.integerToBigNat -> d1) t =
    case m of
-     0# -> panic "ec_twin_mult" ["modulus too large", show (Integer.bigNatToInteger (primeMod p))]
+     0# -> panic "ec_twin_mult" ["modulus too large", show (BN.bigNatToInteger (primeMod p))]
      _  -> go m init_c0 init_c1 zro
 
  where
   (s',t',spt',smt') = normalizeForTwinMult p s t
 
-  m = case max 4 (widthInteger (Integer.bigNatToInteger (primeMod p))) of
-        Integer.S# mint -> mint
+  m = case max 4 (widthInteger (BN.bigNatToInteger (primeMod p))) of
+        BN.IS mint -> mint
         _ -> 0# -- if `m` doesn't fit into an Int, should be impossible
 
   init_c0 = C False False (tst d0 (m -# 1#)) (tst d0 (m -# 2#)) (tst d0 (m -# 3#)) (tst d0 (m -# 4#))
   init_c1 = C False False (tst d1 (m -# 1#)) (tst d1 (m -# 2#)) (tst d1 (m -# 3#)) (tst d1 (m -# 4#))
 
   tst x i
-    | tagToEnum# (i >=# 0#) = Integer.testBitBigNat x i
+    | isTrue# (i >=# 0#) = BN.testBitBigNat x i
     | otherwise = False
 
   f i =
-    if tagToEnum# (i <# 18#) then
-      if tagToEnum# (i <# 12#) then
-        if tagToEnum# (i <# 4#) then
+    if isTrue# (i <# 18#) then
+      if isTrue# (i <# 12#) then
+        if isTrue# (i <# 4#) then
           12#
         else
           14#
       else
-        if tagToEnum# (i <# 14#) then
+        if isTrue# (i <# 14#) then
           12#
         else
           10#
     else
-      if tagToEnum# (i <# 22#) then
+      if isTrue# (i <# 22#) then
         9#
       else
-        if tagToEnum# (i <# 24#) then
+        if isTrue# (i <# 24#) then
           11#
         else
           12#
 
-  go !k !c0 !c1 !r = if tagToEnum# (k <# 0#) then r else go (k -# 1#) c0' c1' r'
+  go !k !c0 !c1 !r = if isTrue# (k <# 0#) then r else go (k -# 1#) c0' c1' r'
     where
       h0  = cStateToH c0
       h1  = cStateToH c1
-      u0  = if tagToEnum# (h0 <# f h1) then 0# else (if cHead c0 then -1# else 1#)
-      u1  = if tagToEnum# (h1 <# f h0) then 0# else (if cHead c1 then -1# else 1#)
+      u0  = if isTrue# (h0 <# f h1) then 0# else (if cHead c0 then -1# else 1#)
+      u1  = if isTrue# (h1 <# f h0) then 0# else (if cHead c1 then -1# else 1#)
       c0' = cStateUpdate u0 c0 (tst d0 (k -# 5#))
       c1' = cStateUpdate u1 c1 (tst d1 (k -# 5#))
 
@@ -571,4 +515,4 @@
 cStateUpdate u (C _ c1 c2 c3 c4 c5) e =
   case u of
     0# -> C c1 c2 c3 c4 c5 e
-    _  -> C (complement c1) c2 c3 c4 c5 e
+    _  -> C (not c1) c2 c3 c4 c5 e
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -14,6 +14,8 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE RecordWildCards #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.REPL.Command (
     -- * Commands
     Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)
@@ -1124,9 +1126,18 @@
 moduleCmd modString
   | null modString = return ()
   | otherwise      = do
-      case parseModName modString of
-        Just m  -> loadHelper (M.loadModuleByName m)
-        Nothing -> rPutStrLn "Invalid module name."
+    case parseModName modString of
+      Just m
+        | M.isParamInstModName m -> loadHelper (M.loadModuleByName m)
+        | otherwise  ->
+          do mpath <- liftModuleCmd (M.findModule m)
+             case mpath of
+               M.InFile file ->
+                 do setEditPath file
+                    setLoadedMod LoadedModule { lName = Just m, lPath = mpath }
+                    loadHelper (M.loadModuleByPath file)
+               M.InMem {} -> loadHelper (M.loadModuleByName m)
+      Nothing -> rPutStrLn "Invalid module name."
 
 loadPrelude :: REPL ()
 loadPrelude  = moduleCmd $ show $ pp M.preludeName
@@ -1246,7 +1257,7 @@
   noInfo nameEnv name =
     case M.nameInfo name of
       M.Declared m _ ->
-                      rPrint $runDoc nameEnv ("Name defined in module" <+> pp m)
+                      rPrint $ runDoc nameEnv ("Name defined in module" <+> pp m)
       M.Parameter  -> rPutStrLn "// No documentation is available."
 
 
@@ -1330,7 +1341,7 @@
          return $
            do rPutStrLn ""
 
-              let property 
+              let property
                     | P.PragmaProperty `elem` ifDeclPragmas = [text "property"]
                     | otherwise                             = []
               rPrint $ runDoc nameEnv
diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@@ -218,7 +218,7 @@
   | detailedPrompt = withEdit ++ "> "
   | otherwise      = modLn ++ "> "
   where
-  detailedPrompt = False
+  detailedPrompt = id False
 
   modLn   =
     case lName =<< eLoadedMod rw of
@@ -266,13 +266,13 @@
 
 instance Applicative REPL where
   {-# INLINE pure #-}
-  pure = return
+  pure x = REPL (\_ -> pure x)
   {-# INLINE (<*>) #-}
   (<*>) = ap
 
 instance Monad REPL where
   {-# INLINE return #-}
-  return x = REPL (\_ -> return x)
+  return = pure
 
   {-# INLINE (>>=) #-}
   m >>= f = REPL $ \ref -> do
diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
--- a/src/Cryptol/Symbolic/SBV.hs
+++ b/src/Cryptol/Symbolic/SBV.hs
@@ -420,7 +420,10 @@
   mkTevs prims result = do
     -- It's a bit fragile, but the value of the safety predicate seems
     -- to always be the first value in the model assignment list.
-    let Right (_, (safetyCV : cvs)) = SBV.getModelAssignment result
+    let (safetyCV, cvs) =
+          case SBV.getModelAssignment result of
+            Right (_, (safetyCV' : cvs')) -> (safetyCV', cvs')
+            _ -> error "processResults: SBV.getModelAssignment failure"
         safety = SBV.cvToBool safetyCV
         (vs, _) = parseValues ts cvs
         mdl = computeModel prims ts vs
diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs
--- a/src/Cryptol/Transform/MonoValues.hs
+++ b/src/Cryptol/Transform/MonoValues.hs
@@ -84,9 +84,10 @@
 import Cryptol.TypeCheck.AST hiding (splitTApp) -- XXX: just use this one
 import Cryptol.TypeCheck.TypeMap
 import Cryptol.Utils.Ident(Namespace(..))
-import Data.List(sortBy,groupBy)
+import Data.List(sortBy)
 import Data.Either(partitionEithers)
 import Data.Map (Map)
+import qualified Data.List.NonEmpty as NE
 import MonadLib hiding (mapM)
 
 import Prelude ()
@@ -224,7 +225,7 @@
     NonRecursive d -> NonRecursive <$> rewD rews d
     Recursive ds ->
       do let (leave,rew) = partitionEithers (map consider ds)
-             rewGroups   = groupBy sameTParams
+             rewGroups   = NE.groupBy sameTParams
                          $ sortBy compareTParams rew
          ds1 <- mapM (rewD rews) leave
          ds2 <- mapM rewSame rewGroups
@@ -243,10 +244,10 @@
                      else Left d
 
   rewSame ds =
-     do new <- forM ds $ \(d,_,_,e) ->
+     do new <- forM (NE.toList ds) $ \(d,_,_,e) ->
                  do x <- newName
                     return (d, x, e)
-        let (_,tps,props,_) : _ = ds
+        let (_,tps,props,_) NE.:| _ = ds
             tys            = map (TVar . tpVar) tps
             proofNum       = length props
             addRew (d,x,_) = insertTM (dName d,tys,proofNum) x
diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs
--- a/src/Cryptol/Transform/Specialize.hs
+++ b/src/Cryptol/Transform/Specialize.hs
@@ -1,3 +1,6 @@
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+
 -- |
 -- Module      :  Cryptol.Transform.Specialize
 -- Copyright   :  (c) 2013-2016 Galois, Inc.
diff --git a/src/Cryptol/TypeCheck/CheckModuleInstance.hs b/src/Cryptol/TypeCheck/CheckModuleInstance.hs
--- a/src/Cryptol/TypeCheck/CheckModuleInstance.hs
+++ b/src/Cryptol/TypeCheck/CheckModuleInstance.hs
@@ -1,4 +1,6 @@
 {-# Language OverloadedStrings #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.TypeCheck.CheckModuleInstance (checkModuleInstance) where
 
 import           Data.Map ( Map )
diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs
--- a/src/Cryptol/TypeCheck/Error.hs
+++ b/src/Cryptol/TypeCheck/Error.hs
@@ -1,6 +1,8 @@
 {-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-}
 {-# Language OverloadedStrings #-}
 {-# Language Safe #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.TypeCheck.Error where
 
 import qualified Data.IntMap as IntMap
@@ -16,6 +18,7 @@
 import Cryptol.TypeCheck.Type
 import Cryptol.TypeCheck.InferTypes
 import Cryptol.TypeCheck.Subst
+import Cryptol.TypeCheck.Unify(Path,isRootPath)
 import Cryptol.ModuleSystem.Name(Name)
 import Cryptol.Utils.Ident(Ident)
 import Cryptol.Utils.RecordMap
@@ -52,7 +55,7 @@
 
 -- | Should the first error suppress the next one.
 subsumes :: (Range,Error) -> (Range,Error) -> Bool
-subsumes (_,NotForAll _ x _) (_,NotForAll _ y _) = x == y
+subsumes (_,NotForAll _ _ x _) (_,NotForAll _ _ y _) = x == y
 subsumes (r1,KindMismatch {}) (r2,err) =
   case err of
     KindMismatch {} -> r1 == r2
@@ -84,10 +87,10 @@
               | RecursiveTypeDecls [Name]
                 -- ^ The type synonym declarations are recursive
 
-              | TypeMismatch TypeSource Type Type
+              | TypeMismatch TypeSource Path Type Type
                 -- ^ Expected type, inferred type
 
-              | RecursiveType TypeSource Type Type
+              | RecursiveType TypeSource Path Type Type
                 -- ^ Unification results in a recursive type
 
               | UnsolvedGoals [Goal]
@@ -105,11 +108,11 @@
                 -- ^ Type wild cards are not allowed in this context
                 -- (e.g., definitions of type synonyms).
 
-              | TypeVariableEscaped TypeSource Type [TParam]
+              | TypeVariableEscaped TypeSource Path Type [TParam]
                 -- ^ Unification variable depends on quantified variables
                 -- that are not in scope.
 
-              | NotForAll TypeSource TVar Type
+              | NotForAll TypeSource Path TVar Type
                 -- ^ Quantified type variables (of kind *) need to
                 -- match the given type, so it does not work for all types.
 
@@ -222,15 +225,15 @@
       TooManyTySynParams {}     -> err
       TooFewTyParams {}         -> err
       RecursiveTypeDecls {}     -> err
-      TypeMismatch src t1 t2    -> TypeMismatch src !$ (apSubst su t1) !$ (apSubst su t2)
-      RecursiveType src t1 t2   -> RecursiveType src !$ (apSubst su t1) !$ (apSubst su t2)
+      TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2)
+      RecursiveType src pa t1 t2   -> RecursiveType src pa !$ (apSubst su t1) !$ (apSubst su t2)
       UnsolvedGoals gs          -> UnsolvedGoals !$ apSubst su gs
       UnsolvableGoals gs        -> UnsolvableGoals !$ apSubst su gs
       UnsolvedDelayedCt g       -> UnsolvedDelayedCt !$ (apSubst su g)
       UnexpectedTypeWildCard    -> err
-      TypeVariableEscaped src t xs ->
-                                 TypeVariableEscaped src !$ (apSubst su t) .$ xs
-      NotForAll src x t         -> NotForAll src x !$ (apSubst su t)
+      TypeVariableEscaped src pa t xs ->
+                                 TypeVariableEscaped src pa !$ (apSubst su t) .$ xs
+      NotForAll src pa x t        -> NotForAll src pa x !$ (apSubst su t)
       TooManyPositionalTypeParams -> err
       CannotMixPositionalAndNamedTypeParams -> err
 
@@ -258,15 +261,15 @@
       TooManyTySynParams {}     -> Set.empty
       TooFewTyParams {}         -> Set.empty
       RecursiveTypeDecls {}     -> Set.empty
-      TypeMismatch _ t1 t2      -> fvs (t1,t2)
-      RecursiveType _ t1 t2     -> fvs (t1,t2)
+      TypeMismatch _ _ t1 t2    -> fvs (t1,t2)
+      RecursiveType _ _ t1 t2   -> fvs (t1,t2)
       UnsolvedGoals gs          -> fvs gs
       UnsolvableGoals gs        -> fvs gs
       UnsolvedDelayedCt g       -> fvs g
       UnexpectedTypeWildCard    -> Set.empty
-      TypeVariableEscaped _ t xs-> fvs t `Set.union`
+      TypeVariableEscaped _ _ t xs-> fvs t `Set.union`
                                             Set.fromList (map TVBound xs)
-      NotForAll _ x t             -> Set.insert x (fvs t)
+      NotForAll _ _ x t             -> Set.insert x (fvs t)
       TooManyPositionalTypeParams -> Set.empty
       CannotMixPositionalAndNamedTypeParams -> Set.empty
       UndefinedTypeParameter {}             -> Set.empty
@@ -308,13 +311,13 @@
   ppPrec _ (WithNames err names) =
     case err of
 
-      RecursiveType src t1 t2 ->
+      RecursiveType src pa t1 t2 ->
         addTVarsDescsAfter names err $
         nested "Matching would result in an infinite type." $
-          vcat [ "The type: " <+> ppWithNames names t1
-               , "occurs in:" <+> ppWithNames names t2
-               , "When checking" <+> pp src
-               ]
+          vcat ( [ "The type: " <+> ppWithNames names t1
+                 , "occurs in:" <+> ppWithNames names t2
+                 ] ++ ppCtxt pa ++
+                 [ "When checking" <+> pp src ] )
 
       UnexpectedTypeWildCard ->
         addTVarsDescsAfter names err $
@@ -357,13 +360,14 @@
         nested "Recursive type declarations:"
                (commaSep $ map nm ts)
 
-      TypeMismatch src t1 t2 ->
+      TypeMismatch src pa t1 t2 ->
         addTVarsDescsAfter names err $
         nested "Type mismatch:" $
         vcat $
           [ "Expected type:" <+> ppWithNames names t1
           , "Inferred type:" <+> ppWithNames names t2
           ] ++ mismatchHint t1 t2
+            ++ ppCtxt pa
             ++ ["When checking" <+> pp src]
 
       UnsolvableGoals gs -> explainUnsolvable names gs
@@ -389,22 +393,24 @@
           nested "while validating user-specified signature" $
           ppWithNames names g
 
-      TypeVariableEscaped src t xs ->
+      TypeVariableEscaped src pa t xs ->
         addTVarsDescsAfter names err $
         nested ("The type" <+> ppWithNames names t <+>
                                         "is not sufficiently polymorphic.") $
-          vcat [ "It cannot depend on quantified variables:" <+>
-                     (commaSep (map (ppWithNames names) xs))
-               , "When checking" <+> pp src
-               ]
+          vcat ( [ "It cannot depend on quantified variables:" <+>
+                       (commaSep (map (ppWithNames names) xs))
+                 ] ++ ppCtxt pa
+                   ++ [ "When checking" <+> pp src ]
+               )
 
-      NotForAll src x t ->
+      NotForAll src pa x t ->
         addTVarsDescsAfter names err $
         nested "Inferred type is not sufficiently polymorphic." $
-          vcat [ "Quantified variable:" <+> ppWithNames names x
-               , "cannot match type:"   <+> ppWithNames names t
-               , "When checking" <+> pp src
-               ]
+          vcat ( [ "Quantified variable:" <+> ppWithNames names x
+                 , "cannot match type:"   <+> ppWithNames names t
+                 ] ++ ppCtxt pa
+                   ++ [ "When checking" <+> pp src ]
+               )
 
       BadParameterKind tp k ->
         addTVarsDescsAfter names err $
@@ -479,8 +485,11 @@
 
     noUni = Set.null (Set.filter isFreeTV (fvs err))
 
+    ppCtxt pa = if isRootPath pa then [] else [ "Context:" <+> pp pa ]
 
 
+
+
 explainUnsolvable :: NameMap -> [Goal] -> Doc
 explainUnsolvable names gs =
   addTVarsDescsAfter names gs (bullets (map explain gs))
@@ -497,7 +506,9 @@
     case tNoUser (goal g) of
       TCon (PC pc) ts ->
         let tys = [ backticks (ppWithNames names t) | t <- ts ]
-            doc1 : _ = tys
+            doc1 = case tys of
+                     (doc1' : _) -> doc1'
+                     [] -> error "explainUnsolvable: Expected TCon to have at least one argument"
             custom msg = hang msg
                             2 (text "arising from" $$
                                pp (goalSource g)   $$
@@ -563,7 +574,7 @@
 
           PValidFloat ->
             case ts of
-              ~[e,p] -> 
+              ~[e,p] ->
                 custom (hang "Unsupported floating point parameters:"
                            2 ("exponent =" <+> ppWithNames names e $$
                               "precision =" <+> ppWithNames names p))
diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@@ -15,6 +15,8 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE Safe #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.TypeCheck.Infer
   ( checkE
   , checkSigB
@@ -44,6 +46,7 @@
                                         checkParameterConstraints)
 import           Cryptol.TypeCheck.Instantiate
 import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
+import           Cryptol.TypeCheck.Unify(rootPath)
 import           Cryptol.Utils.Ident
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.RecordMap
@@ -58,7 +61,7 @@
 import           Data.Ratio(numerator,denominator)
 import           Data.Traversable(forM)
 import           Data.Function(on)
-import           Control.Monad(zipWithM,unless,foldM,forM_)
+import           Control.Monad(zipWithM,unless,foldM,forM_,mplus)
 
 
 
@@ -247,13 +250,14 @@
 
     P.ETuple es ->
       do etys <- expectTuple (length es) tGoal
-         let mkTGoal n t = WithSource t (TypeOfTupleField n)
-         es'  <- zipWithM checkE es (zipWith mkTGoal [1..] etys)
+         let mkTGoal n t e = WithSource t (TypeOfTupleField n) (getLoc e)
+         es'  <- zipWithM checkE es (zipWith3 mkTGoal [1..] etys es)
          return (ETuple es')
 
     P.ERecord fs ->
       do es  <- expectRec fs tGoal
-         let checkField f (e,t) = checkE e (WithSource t (TypeOfRecordField f))
+         let checkField f (e,t) =
+                checkE e (WithSource t (TypeOfRecordField f) (getLoc e))
          es' <- traverseRecordMap checkField es
          return (ERec es')
 
@@ -262,19 +266,19 @@
     P.ESel e l ->
       do let src = selSrc l
          t <- newType src KType
-         e' <- checkE e (WithSource t src)
+         e' <- checkE e (WithSource t src (getLoc expr))
          f <- newHasGoal l t (twsType tGoal)
          return (hasDoSelect f e')
 
     P.EList [] ->
       do (len,a) <- expectSeq tGoal
-         expectFin 0 (WithSource len LenOfSeq)
+         expectFin 0 (WithSource len LenOfSeq (getLoc expr))
          return (EList [] a)
 
     P.EList es ->
       do (len,a) <- expectSeq tGoal
-         expectFin (length es) (WithSource len LenOfSeq)
-         let checkElem e = checkE e (WithSource a TypeOfSeqElement)
+         expectFin (length es) (WithSource len LenOfSeq (getLoc expr))
+         let checkElem e = checkE e (WithSource a TypeOfSeqElement (getLoc e))
          es' <- mapM checkElem es
          return (EList es' a)
 
@@ -378,11 +382,12 @@
          (len,a) <- expectSeq tGoal
 
          inferred <- smallest ts
-         ctrs <- unify (WithSource len LenOfSeq) inferred
+         ctrs <- unify (WithSource len LenOfSeq (getLoc expr)) inferred
          newGoals CtComprehension ctrs
 
          ds     <- combineMaps dss
-         e'     <- withMonoTypes ds (checkE e (WithSource a TypeOfSeqElement))
+         e'     <- withMonoTypes ds (checkE e
+                                (WithSource a TypeOfSeqElement (getLoc e)))
          return (EComp len a e' mss')
       where
       -- the renamer should have made these checks already?
@@ -407,12 +412,13 @@
     P.EApp e1 e2 ->
       do let argSrc = TypeOfArg noArgDescr
          t1  <- newType argSrc  KType
-         e1' <- checkE e1 (WithSource (tFun t1 (twsType tGoal)) FunApp)
-         e2' <- checkE e2 (WithSource t1 argSrc)
+         e1' <- checkE e1
+                  (WithSource (tFun t1 (twsType tGoal)) FunApp (getLoc e1))
+         e2' <- checkE e2 (WithSource t1 argSrc (getLoc e2))
          return (EApp e1' e2')
 
     P.EIf e1 e2 e3 ->
-      do e1'      <- checkE e1 (WithSource tBit TypeOfIfCondExpr)
+      do e1'      <- checkE e1 (WithSource tBit TypeOfIfCondExpr (getLoc e1))
          e2'      <- checkE e2 tGoal
          e3'      <- checkE e3 tGoal
          return (EIf e1' e2' e3')
@@ -423,7 +429,7 @@
 
     P.ETyped e t ->
       do tSig <- checkTypeOfKind t KType
-         e' <- checkE e (WithSource tSig TypeFromUserAnnotation)
+         e' <- checkE e (WithSource tSig TypeFromUserAnnotation (getLoc expr))
          checkHasType tSig tGoal
          return e'
 
@@ -465,28 +471,28 @@
 
     Just e ->
       do e1 <- checkE e tGoal
-         foldM doUpd e1 fs
+         fst <$> foldM doUpd (e1, getLoc e) fs
 
   where
-  doUpd e (P.UpdField how sels v) =
+  doUpd (e,eloc) (P.UpdField how sels v) =
     case sels of
       [l] ->
         case how of
           P.UpdSet ->
             do let src = selSrc s
                ft <- newType src KType
-               v1 <- checkE v (WithSource ft src)
+               v1 <- checkE v (WithSource ft src eloc)
                d  <- newHasGoal s (twsType tGoal) ft
-               pure (hasDoSet d e v1)
+               pure (hasDoSet d e v1, eloc `rCombMaybe` getLoc v)
           P.UpdFun ->
              do let src = selSrc s
                 ft <- newType src KType
-                v1 <- checkE v (WithSource (tFun ft ft) src)
+                v1 <- checkE v (WithSource (tFun ft ft) src eloc)
                 -- XXX: ^ may be used a different src?
                 d  <- newHasGoal s (twsType tGoal) ft
                 tmp <- newParamName NSValue (packIdent "rf")
                 let e' = EVar tmp
-                pure $ hasDoSet d e' (EApp v1 (hasDoSelect d e'))
+                pure ( hasDoSet d e' (EApp v1 (hasDoSelect d e'))
                        `EWhere`
                        [  NonRecursive
                           Decl { dName        = tmp
@@ -497,6 +503,7 @@
                                , dFixity      = Nothing
                                , dDoc         = Nothing
                                } ]
+                      , eloc `rCombMaybe` getLoc v )
 
         where s = thing l
       _ -> panic "checkRecUpd/doUpd" [ "Expected exactly 1 field label"
@@ -505,11 +512,11 @@
 
 
 expectSeq :: TypeWithSource -> InferM (Type,Type)
-expectSeq tGoal@(WithSource ty src) =
+expectSeq tGoal@(WithSource ty src rng) =
   case ty of
 
     TUser _ _ ty' ->
-         expectSeq (WithSource ty' src)
+         expectSeq (WithSource ty' src rng)
 
     TCon (TC TCSeq) [a,b] ->
          return (a,b)
@@ -521,7 +528,7 @@
 
     _ ->
       do tys@(a,b) <- genTys
-         recordError (TypeMismatch src ty (tSeq a b))
+         recordErrorLoc rng (TypeMismatch src rootPath ty (tSeq a b))
          return tys
   where
   genTys =
@@ -531,11 +538,11 @@
 
 
 expectTuple :: Int -> TypeWithSource -> InferM [Type]
-expectTuple n tGoal@(WithSource ty src) =
+expectTuple n tGoal@(WithSource ty src rng) =
   case ty of
 
     TUser _ _ ty' ->
-         expectTuple n (WithSource ty' src)
+         expectTuple n (WithSource ty' src rng)
 
     TCon (TC (TCTuple n')) tys | n == n' ->
          return tys
@@ -547,7 +554,7 @@
 
     _ ->
       do tys <- genTys
-         recordError (TypeMismatch src ty (tTuple tys))
+         recordErrorLoc rng (TypeMismatch src rootPath ty (tTuple tys))
          return tys
 
   where
@@ -558,11 +565,11 @@
   RecordMap Ident (Range, a) ->
   TypeWithSource ->
   InferM (RecordMap Ident (a, Type))
-expectRec fs tGoal@(WithSource ty src) =
+expectRec fs tGoal@(WithSource ty src rng) =
   case ty of
 
     TUser _ _ ty' ->
-         expectRec fs (WithSource ty' src)
+         expectRec fs (WithSource ty' src rng)
 
     TRec ls
       | Right r <- zipRecords (\_ (_rng,v) t -> (v,t)) fs ls -> pure r
@@ -577,16 +584,16 @@
          case ty of
            TVar TVFree{} -> do ps <- unify tGoal (TRec tys)
                                newGoals CtExactType ps
-           _ -> recordError (TypeMismatch src ty (TRec tys))
+           _ -> recordErrorLoc rng (TypeMismatch src rootPath ty (TRec tys))
          return res
 
 
 expectFin :: Int -> TypeWithSource -> InferM ()
-expectFin n tGoal@(WithSource ty src) =
+expectFin n tGoal@(WithSource ty src rng) =
   case ty of
 
     TUser _ _ ty' ->
-         expectFin n (WithSource ty' src)
+         expectFin n (WithSource ty' src rng)
 
     TCon (TC (TCNum n')) [] | toInteger n == n' ->
          return ()
@@ -594,7 +601,7 @@
     _ -> newGoals CtExactType =<< unify tGoal (tNum n)
 
 expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Type],Type)
-expectFun mbN n (WithSource ty0 src)  = go [] n ty0
+expectFun mbN n (WithSource ty0 src rng)  = go [] n ty0
   where
 
   go tys arity ty
@@ -612,9 +619,10 @@
              res  <- newType TypeOfRes KType
              case ty of
                TVar TVFree{} ->
-                  do ps <- unify (WithSource ty src) (foldr tFun res args)
+                  do ps <- unify (WithSource ty src rng) (foldr tFun res args)
                      newGoals CtExactType  ps
-               _ -> recordError (TypeMismatch src ty (foldr tFun res args))
+               _ -> recordErrorLoc rng
+                        (TypeMismatch src rootPath ty (foldr tFun res args))
              return (reverse tys ++ args, res)
 
     | otherwise =
@@ -641,9 +649,11 @@
   do let descs = [ TypeOfArg (ArgDescr fun (Just n)) | n <- [ 1 + offset .. ] ]
 
      (tys,tRes) <- expectFun fun (length ps) tGoal
-     largs      <- sequence (zipWith checkP ps (zipWith WithSource tys descs))
+     let srcs = zipWith3 WithSource tys descs (map getLoc ps)
+     largs      <- sequence (zipWith checkP ps srcs)
      let ds = Map.fromList [ (thing x, x { thing = t }) | (x,t) <- zip largs tys ]
-     e1         <- withMonoTypes ds (checkE e (WithSource tRes TypeOfRes))
+     e1 <- withMonoTypes ds
+              (checkE e (WithSource tRes TypeOfRes (twsRange tGoal)))
 
      let args = [ (thing x, t) | (x,t) <- zip largs tys ]
      return (foldr (\(x,t) b -> EAbs x t b) e1 args)
@@ -658,11 +668,12 @@
                    return a
 
 checkP :: P.Pattern Name -> TypeWithSource -> InferM (Located Name)
-checkP p tGoal@(WithSource _ src) =
+checkP p tGoal@(WithSource _ src rng0) =
   do (x, t) <- inferP p
      ps <- unify tGoal (thing t)
-     let rng   = fromMaybe emptyRange (getLoc p)
-     let mkErr = recordError . UnsolvedGoals . (:[])
+     let rngMb = getLoc p `mplus` rng0
+         rng   = fromMaybe emptyRange rngMb
+     let mkErr = recordErrorLoc rngMb . UnsolvedGoals . (:[])
                                                    . Goal (CtPattern src) rng
      mapM_ mkErr ps
      return (Located (srcRange t) x)
@@ -679,7 +690,7 @@
 
     P.PTyped p t ->
       do tSig <- checkTypeOfKind t KType
-         ln   <- checkP p (WithSource tSig TypeFromUserAnnotation)
+         ln   <- checkP p (WithSource tSig TypeFromUserAnnotation (getLoc t))
          return (thing ln, ln { thing = tSig })
 
     _ -> tcPanic "inferP" [ "Unexpected pattern:", show pat ]
@@ -691,7 +702,8 @@
 inferMatch (P.Match p e) =
   do (x,t) <- inferP p
      n     <- newType LenOfCompGen KNum
-     e'    <- checkE e (WithSource (tSeq n (thing t)) GeneratorOfListComp)
+     e'    <- checkE e (WithSource (tSeq n (thing t)) GeneratorOfListComp
+                                   (getLoc e))
      return (From x n (thing t) e', x, t, n)
 
 inferMatch (P.MatchLet b)
@@ -943,7 +955,7 @@
 
     P.DExpr e ->
       do let nm = thing (P.bName b)
-         let tGoal = WithSource t (DefinitionOf nm)
+         let tGoal = WithSource t (DefinitionOf nm) (getLoc b)
          e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e tGoal
          let f = thing (P.bName b)
          return Decl { dName = f
@@ -975,7 +987,7 @@
   withTParams as $
   do (e1,cs0) <- collectGoals $
                 do let nm = thing (P.bName b)
-                       tGoal = WithSource t0 (DefinitionOf nm)
+                       tGoal = WithSource t0 (DefinitionOf nm) (getLoc b)
                    e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e0 tGoal
                    addGoals validSchema
                    () <- simplifyAllConstraints  -- XXX: using `asmps` also?
diff --git a/src/Cryptol/TypeCheck/Instantiate.hs b/src/Cryptol/TypeCheck/Instantiate.hs
--- a/src/Cryptol/TypeCheck/Instantiate.hs
+++ b/src/Cryptol/TypeCheck/Instantiate.hs
@@ -205,5 +205,6 @@
     | Set.notMember tp bounds = return []
     | otherwise = let a   = tpVar tp
                       src = tvarDesc (tvInfo a)
-                  in unify (WithSource (TVar a) src) ty
+                      rng = Just (tvarSource (tvInfo a))
+                  in unify (WithSource (TVar a) src rng) ty
 
diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs
--- a/src/Cryptol/TypeCheck/Kind.hs
+++ b/src/Cryptol/TypeCheck/Kind.hs
@@ -8,6 +8,8 @@
 
 {-# LANGUAGE RecursiveDo #-}
 {-# LANGUAGE Safe #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.TypeCheck.Kind
   ( checkType
   , checkSchema
@@ -302,7 +304,8 @@
     do let ty = tpVar (mtpParam a)
        (ts1,k1) <- appTy ts (kindOf ty)
        case k of
-         Just ks | ks /= k1 -> kRecordError $ KindMismatch Nothing ks k1
+         Just ks
+           | ks /= k1 -> kRecordError (KindMismatch Nothing ks k1)
          _ -> return ()
 
        unless (null ts1) $
diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs
--- a/src/Cryptol/TypeCheck/Monad.hs
+++ b/src/Cryptol/TypeCheck/Monad.hs
@@ -45,7 +45,8 @@
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Subst
 import           Cryptol.TypeCheck.Interface(genIface)
-import           Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))
+import           Cryptol.TypeCheck.Unify(doMGU, runResult, UnificationError(..)
+                                        , Path, rootPath)
 import           Cryptol.TypeCheck.InferTypes
 import           Cryptol.TypeCheck.Error( Warning(..),Error(..)
                                         , cleanupErrors, computeFreeVarNames
@@ -292,11 +293,11 @@
   fmap f (IM m) = IM (fmap f m)
 
 instance A.Applicative InferM where
-  pure  = return
+  pure x = IM (pure x)
   (<*>) = ap
 
 instance Monad InferM where
-  return x      = IM (return x)
+  return        = pure
   IM m >>= f    = IM (m >>= unIM . f)
 
 instance Fail.MonadFail InferM where
@@ -331,12 +332,21 @@
 
 -- | Report an error.
 recordError :: Error -> InferM ()
-recordError e =
-  do r <- case e of
-            AmbiguousSize d _ -> return (tvarSource d)
-            _ -> curRange
+recordError = recordErrorLoc Nothing
+
+-- | Report an error.
+recordErrorLoc :: Maybe Range -> Error -> InferM ()
+recordErrorLoc rng e =
+  do r <- case rng of
+            Just r  -> pure r
+            Nothing -> case e of
+                         AmbiguousSize d _ -> return (tvarSource d)
+                         _                 -> curRange
      IM $ sets_ $ \s -> s { iErrors = (r,e) : iErrors s }
 
+
+
+
 recordWarning :: Warning -> InferM ()
 recordWarning w =
   unless ignore $
@@ -549,23 +559,23 @@
 
 -- | Record that the two types should be syntactically equal.
 unify :: TypeWithSource -> Type -> InferM [Prop]
-unify (WithSource t1 src) t2 =
+unify (WithSource t1 src rng) t2 =
   do t1' <- applySubst t1
      t2' <- applySubst t2
-     let ((su1, ps), errs) = runResult (mgu t1' t2')
+     let ((su1, ps), errs) = runResult (doMGU t1' t2')
      extendSubst su1
-     let toError :: UnificationError -> Error
-         toError err =
+     let toError :: (Path,UnificationError) -> Error
+         toError (pa,err) =
            case err of
-             UniTypeLenMismatch _ _ -> TypeMismatch src t1' t2'
-             UniTypeMismatch s1 s2  -> TypeMismatch src s1 s2
+             UniTypeLenMismatch _ _ -> TypeMismatch src rootPath t1' t2'
+             UniTypeMismatch s1 s2  -> TypeMismatch src pa s1 s2
              UniKindMismatch k1 k2  -> KindMismatch (Just src) k1 k2
-             UniRecursive x t       -> RecursiveType src (TVar x) t
-             UniNonPolyDepends x vs -> TypeVariableEscaped src (TVar x) vs
-             UniNonPoly x t         -> NotForAll src x t
+             UniRecursive x t       -> RecursiveType src pa (TVar x) t
+             UniNonPolyDepends x vs -> TypeVariableEscaped src pa (TVar x) vs
+             UniNonPoly x t         -> NotForAll src pa x t
      case errs of
        [] -> return ps
-       _  -> do mapM_ (recordError . toError) errs
+       _  -> do mapM_ (recordErrorLoc rng . toError) errs
                 return []
 
 -- | Apply the accumulated substitution to something with free type variables.
@@ -958,11 +968,11 @@
   fmap f (KM m) = KM (fmap f m)
 
 instance A.Applicative KindM where
-  pure  = return
+  pure x = KM (pure x)
   (<*>) = ap
 
 instance Monad KindM where
-  return x      = KM (return x)
+  return        = pure
   KM m >>= k    = KM (m >>= unKM . k)
 
 instance Fail.MonadFail KindM where
diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs
--- a/src/Cryptol/TypeCheck/Sanity.hs
+++ b/src/Cryptol/TypeCheck/Sanity.hs
@@ -472,11 +472,11 @@
   fmap = liftM
 
 instance A.Applicative TcM where
-  pure  = return
+  pure a = TcM (pure a)
   (<*>) = ap
 
 instance Monad TcM where
-  return a    = TcM (return a)
+  return      = pure
   TcM m >>= f = TcM (do a <- m
                         let TcM m1 = f a
                         m1)
diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs
--- a/src/Cryptol/TypeCheck/SimpType.hs
+++ b/src/Cryptol/TypeCheck/SimpType.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE PatternGuards #-}
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.TypeCheck.SimpType where
 
 import Control.Applicative((<|>))
diff --git a/src/Cryptol/TypeCheck/SimpleSolver.hs b/src/Cryptol/TypeCheck/SimpleSolver.hs
--- a/src/Cryptol/TypeCheck/SimpleSolver.hs
+++ b/src/Cryptol/TypeCheck/SimpleSolver.hs
@@ -34,7 +34,10 @@
 
   where
   dbg msg x
-    | False     = ppTrace msg x
+      -- Change `False` to `True` below to enable extra tracing. Note that
+      -- this is written with an extraneous `id` expression to suppress
+      -- pattern-match coverage checking warnings in this one case.
+    | id False  = ppTrace msg x
     | otherwise = x
 
 
diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs
--- a/src/Cryptol/TypeCheck/Solver/Numeric.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs
@@ -9,8 +9,7 @@
 import           Data.List (sortBy)
 import           Data.MemoTrie
 
-import qualified GHC.Integer.GMP.Internals as Integer
-
+import Math.NumberTheory.Primes.Testing (isPrime)
 
 import Cryptol.Utils.Patterns
 import Cryptol.TypeCheck.Type hiding (tMul)
@@ -78,11 +77,6 @@
 {-# NOINLINE primeTable #-}
 primeTable :: Integer :->: Bool
 primeTable = trie isPrime
-  where
-    isPrime i =
-      case Integer.testPrimeInteger i 25# of
-        0# -> False
-        _  -> True
 
 cryIsPrime :: Ctxt -> Type -> Solved
 cryIsPrime _varInfo ty =
diff --git a/src/Cryptol/TypeCheck/Solver/Selector.hs b/src/Cryptol/TypeCheck/Solver/Selector.hs
--- a/src/Cryptol/TypeCheck/Solver/Selector.hs
+++ b/src/Cryptol/TypeCheck/Solver/Selector.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE PatternGuards, Safe #-}
 module Cryptol.TypeCheck.Solver.Selector (tryHasGoal) where
 
+import Cryptol.Parser.Position(Range)
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.InferTypes
 import Cryptol.TypeCheck.Monad( InferM, unify, newGoals
@@ -41,8 +42,8 @@
      return (tSeq (tNum n) elems)
 
 
-improveSelector :: Selector -> Type -> InferM Bool
-improveSelector sel outerT =
+improveSelector :: Maybe Range -> Selector -> Type -> InferM Bool
+improveSelector rng sel outerT =
   case sel of
     RecordSel _ mb -> cvt recordType mb
     TupleSel  _ mb -> cvt tupleType  mb
@@ -50,7 +51,7 @@
   where
   cvt _ Nothing   = return False
   cvt f (Just a)  = do ty <- f a
-                       ps <- unify (WithSource outerT (selSrc sel)) ty
+                       ps <- unify (WithSource outerT (selSrc sel) rng) ty
                        newGoals CtExactType ps
                        newT <- applySubst outerT
                        return (newT /= outerT)
@@ -117,13 +118,15 @@
 tryHasGoal :: HasGoal -> InferM (Bool, Bool) -- ^ changes, solved
 tryHasGoal has
   | TCon (PC (PHas sel)) [ th, ft ] <- goal (hasGoal has) =
-    do imped     <- improveSelector sel th
+    do let rng = Just (goalRange (hasGoal has))
+       imped     <- improveSelector rng sel th
        outerT    <- tNoUser `fmap` applySubst th
        mbInnerT  <- solveSelector sel outerT
        case mbInnerT of
          Nothing -> return (imped, False)
          Just innerT ->
-           do newGoals CtExactType =<< unify (WithSource innerT (selSrc sel)) ft
+           do newGoals CtExactType =<<
+                                  unify (WithSource innerT (selSrc sel) rng) ft
               oT <- applySubst outerT
               iT <- applySubst innerT
               sln <- mkSelSln sel oT iT
diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs
--- a/src/Cryptol/TypeCheck/Type.hs
+++ b/src/Cryptol/TypeCheck/Type.hs
@@ -231,6 +231,7 @@
 data TypeWithSource = WithSource
   { twsType   :: Type
   , twsSource :: TypeSource
+  , twsRange  :: !(Maybe Range)
   }
 
 
diff --git a/src/Cryptol/TypeCheck/TypePat.hs b/src/Cryptol/TypeCheck/TypePat.hs
--- a/src/Cryptol/TypeCheck/TypePat.hs
+++ b/src/Cryptol/TypeCheck/TypePat.hs
@@ -1,3 +1,5 @@
+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns]
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 module Cryptol.TypeCheck.TypePat
   ( aInf, aNat, aNat'
 
@@ -193,4 +195,26 @@
                     _                                     -> mzero
 
 
+{-
+Note [-Wincomplete-uni-patterns and irrefutable patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Various parts of Cryptol use irrefutable patterns in functions that assume that
+their arguments have particular shapes. For example, the `ar1 ~[a] = a`
+function in this module uses an irrefutable pattern because it assumes the
+invariant that the argument list will have exactly one element. This lets ar1
+be slightly lazier when evaluated.
 
+Unfortunately, this use of irrefutable patterns is at odds with the
+-Wincomplete-uni-patterns warning. At present, -Wincomplete-uni-patterns will
+produce a warning for any irrefutable pattern that does not cover all possible
+data constructors. While we could rewrite functions like `ar1` to explicitly
+provide a fall-through case, that would change its strictness properties. As
+a result, we simply disable -Wincomplete-uni-patterns warnings in each part
+of Cryptol that uses irrefutable patterns.
+
+Arguably, -Wincomplete-uni-patterns shouldn't be producing warnings for
+irrefutable patterns at all. GHC issue #14800
+(https://gitlab.haskell.org/ghc/ghc/-/issues/14800) proposes this idea.
+If that issue is fixed in the future, we may want to reconsider whether we want
+to disable -Wincomplete-uni-patterns.
+-}
diff --git a/src/Cryptol/TypeCheck/Unify.hs b/src/Cryptol/TypeCheck/Unify.hs
--- a/src/Cryptol/TypeCheck/Unify.hs
+++ b/src/Cryptol/TypeCheck/Unify.hs
@@ -8,13 +8,20 @@
 
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE PatternGuards, ViewPatterns #-}
-{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFunctor, DeriveGeneric, DeriveAnyClass #-}
+{-# LANGUAGE BlockArguments, OverloadedStrings #-}
 module Cryptol.TypeCheck.Unify where
 
+import Control.DeepSeq(NFData)
+import GHC.Generics(Generic)
+
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Subst
 import Cryptol.Utils.RecordMap
+import Cryptol.Utils.Ident(Ident)
+import Cryptol.ModuleSystem.Name(nameIdent)
 
+import Cryptol.TypeCheck.PP
 import Control.Monad.Writer (Writer, writer, runWriter)
 import qualified Data.Set as Set
 
@@ -25,9 +32,9 @@
 -- on bound variables.
 type MGU = (Subst,[Prop])
 
-type Result a = Writer [UnificationError] a
+type Result a = Writer [(Path,UnificationError)] a
 
-runResult :: Result a -> (a, [UnificationError])
+runResult :: Result a -> (a, [(Path,UnificationError)])
 runResult = runWriter
 
 data UnificationError
@@ -38,31 +45,56 @@
   | UniNonPolyDepends TVar [TParam]
   | UniNonPoly TVar Type
 
-uniError :: UnificationError -> Result MGU
-uniError e = writer (emptyMGU, [e])
+uniError :: Path -> UnificationError -> Result MGU
+uniError p e = writer (emptyMGU, [(p,e)])
 
 
+newtype Path = Path [PathElement]
+  deriving (Show,Generic,NFData)
+
+data PathElement =
+    TConArg     TC      Int
+  | TNewtypeArg Newtype Int
+  | TRecArg     Ident
+  deriving (Show,Generic,NFData)
+
+rootPath :: Path
+rootPath = Path []
+
+isRootPath :: Path -> Bool
+isRootPath (Path xs) = null xs
+
+extPath :: Path -> PathElement -> Path
+extPath (Path xs) x = Path (x : xs)
+
+
 emptyMGU :: MGU
 emptyMGU = (emptySubst, [])
 
-mgu :: Type -> Type -> Result MGU
+doMGU :: Type -> Type -> Result MGU
+doMGU t1 t2 = mgu rootPath t1 t2
 
-mgu (TUser c1 ts1 _) (TUser c2 ts2 _)
+mgu :: Path -> Type -> Type -> Result MGU
+
+mgu _ (TUser c1 ts1 _) (TUser c2 ts2 _)
   | c1 == c2 && ts1 == ts2  = return emptyMGU
 
-mgu (TVar x) t        = bindVar x t
-mgu t (TVar x)        = bindVar x t
+mgu p (TVar x) t     = bindVar p x t
+mgu p t (TVar x)     = bindVar p x t
 
-mgu (TUser _ _ t1) t2 = mgu t1 t2
-mgu t1 (TUser _ _ t2) = mgu t1 t2
+mgu p (TUser _ _ t1) t2 = mgu p t1 t2
+mgu p t1 (TUser _ _ t2) = mgu p t1 t2
 
-mgu (TCon (TC tc1) ts1) (TCon (TC tc2) ts2)
-  | tc1 == tc2 = mguMany ts1 ts2
+mgu p (TCon (TC tc1) ts1) (TCon (TC tc2) ts2)
+  | tc1 == tc2 =
+    let paths = [ extPath p (TConArg tc1 i) | i <- [ 0 .. ] ]
+    in mguMany p paths ts1 ts2
 
-mgu (TCon (TF f1) ts1) (TCon (TF f2) ts2)
+mgu _ (TCon (TF f1) ts1) (TCon (TF f2) ts2)
   | f1 == f2 && ts1 == ts2  = return emptyMGU
 
-mgu t1 t2
+-- XXX: here we loose the information about where the constarint came from
+mgu _ t1 t2
   | TCon (TF _) _ <- t1, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2])
   | TCon (TF _) _ <- t2, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2])
   where
@@ -71,58 +103,114 @@
 
   isNum = k1 == KNum
 
-mgu (TRec fs1) (TRec fs2)
-  | fieldSet fs1 == fieldSet fs2 = mguMany (recordElements fs1) (recordElements fs2)
+mgu p (TRec fs1) (TRec fs2)
+  | fieldSet fs1 == fieldSet fs2 =
+    let paths = [ extPath p (TRecArg i) | (i,_) <- canonicalFields fs1 ]
+    in mguMany p paths (recordElements fs1) (recordElements fs2)
 
-mgu (TNewtype ntx xs) (TNewtype nty ys)
-  | ntx == nty = mguMany xs ys
+mgu p (TNewtype ntx xs) (TNewtype nty ys)
+  | ntx == nty =
+    let paths = [ extPath p (TNewtypeArg ntx i) | i <- [ 0 .. ] ]
+    in mguMany p paths xs ys
 
-mgu t1 t2
-  | not (k1 == k2)  = uniError $ UniKindMismatch k1 k2
-  | otherwise       = uniError $ UniTypeMismatch t1 t2
+mgu p t1 t2
+  | not (k1 == k2)  = uniError p $ UniKindMismatch k1 k2
+  | otherwise       = uniError p $ UniTypeMismatch t1 t2
   where
   k1 = kindOf t1
   k2 = kindOf t2
 
 
-mguMany :: [Type] -> [Type] -> Result MGU
-mguMany [] [] = return emptyMGU
-mguMany (t1 : ts1) (t2 : ts2) =
-  do (su1,ps1) <- mgu t1 t2
-     (su2,ps2) <- mguMany (apSubst su1 ts1) (apSubst su1 ts2)
+-- XXX: could pass the path to the lists themselvs
+mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU
+mguMany _ _ [] [] = return emptyMGU
+mguMany p (p1:ps) (t1 : ts1) (t2 : ts2) =
+  do (su1,ps1) <- mgu p1 t1 t2
+     (su2,ps2) <- mguMany p ps (apSubst su1 ts1) (apSubst su1 ts2)
      return (su2 @@ su1, ps1 ++ ps2)
-mguMany t1 t2 = uniError $ UniTypeLenMismatch (length t1) (length t2)
+mguMany p _ t1 t2 = uniError p $ UniTypeLenMismatch (length t1) (length t2)
+-- XXX: I think by this point the types should have been kind checked,
+-- so there should be no mismatches with the lengths...
 
 
-bindVar :: TVar -> Type -> Result MGU
+bindVar :: Path -> TVar -> Type -> Result MGU
 
-bindVar x (tNoUser -> TVar y)
+bindVar _ x (tNoUser -> TVar y)
   | x == y                      = return emptyMGU
 
-bindVar v@(TVBound {}) (tNoUser -> TVar v1@(TVFree {})) = bindVar v1 (TVar v)
+bindVar p v@(TVBound {})
+          (tNoUser -> TVar v1@(TVFree {})) = bindVar p v1 (TVar v)
 
-bindVar v@(TVBound {}) t
+bindVar p v@(TVBound {}) t
   | k == kindOf t = if k == KNum
                        then return (emptySubst, [TVar v =#= t])
-                       else uniError $ UniNonPoly v t
-  | otherwise     = uniError $ UniKindMismatch k (kindOf t)
+                       else uniError p $ UniNonPoly v t
+  | otherwise     = uniError p $ UniKindMismatch k (kindOf t)
   where k = kindOf v
 
-bindVar x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _))
+bindVar _ x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _))
   | xscope `Set.isProperSubsetOf` yscope, xk == yk =
     return (uncheckedSingleSubst y (TVar x), [])
     -- In this case, we can add the reverse binding y ~> x to the
     -- substitution, but the instantiation x ~> y would be forbidden
     -- because it would allow y to escape from its scope.
 
-bindVar x t =
+bindVar p x t =
   case singleSubst x t of
     Left SubstRecursive
-      | kindOf x == KType -> uniError $ UniRecursive x t
+      | kindOf x == KType -> uniError p $ UniRecursive x t
       | otherwise -> return (emptySubst, [TVar x =#= t])
     Left (SubstEscaped tps) ->
-      uniError $ UniNonPolyDepends x tps
+      uniError p $ UniNonPolyDepends x tps
     Left (SubstKindMismatch k1 k2) ->
-      uniError $ UniKindMismatch k1 k2
+      uniError p $ UniKindMismatch k1 k2
     Right su ->
       return (su, [])
+
+
+--------------------------------------------------------------------------------
+
+ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc
+ppPathEl el prec k =
+  case el of
+    TRecArg l -> braces (pp l <+> ":" <+> k 0 <.> comma <+> "…")
+
+    TConArg tc n ->
+      case tc of
+
+       TCSeq -> optParens (prec > 4)
+                if n == 0 then brackets (k 0) <+> "_"
+                          else brackets "_" <+> (k 4)
+
+       TCFun -> optParens (prec > 1)
+                if n == 0 then k 2 <+> "->" <+> "_"
+                          else "_" <+> "->" <+> k 1
+
+       TCTuple i  -> parens (commaSep (before ++ [k 0] ++ after))
+          where before = replicate n "_"
+                after  = replicate (i - n - 1) "_"
+
+       _ -> justPrefix (kindArity (kindOf tc)) (pp tc) n
+
+    TNewtypeArg nt n ->
+      justPrefix (length (ntParams nt)) (pp (nameIdent (ntName nt))) n
+
+  where
+  justPrefix arity fun n =
+    optParens (prec > 3) (fun <+> hsep (before ++ [k 5] ++ after))
+    where before = replicate n "_"
+          after  = replicate (arity - n - 1) "_"
+
+  kindArity ki =
+    case ki of
+      _ :-> k1 -> 1 + kindArity k1
+      _        -> 0
+
+instance PP Path where
+  ppPrec prec0 (Path ps0) = go (reverse ps0) prec0
+    where
+    go ps prec =
+      case ps of
+        []       -> "ERROR"
+        p : more -> ppPathEl p prec (go more)
+
diff --git a/src/GHC/Num/Compat.hs b/src/GHC/Num/Compat.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Num/Compat.hs
@@ -0,0 +1,155 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE UnboxedSums #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+-- |
+-- Module      :  GHC.Num.Compat
+-- Description :  Defines numeric compatibility shims that work with both
+--                ghc-bignum (GHC 9.0+) and integer-gmp (older GHCs).
+-- Copyright   :  (c) 2021 Galois, Inc.
+-- License     :  BSD3
+-- Maintainer  :  cryptol@galois.com
+-- Stability   :  provisional
+-- Portability :  portable
+module GHC.Num.Compat
+  ( -- * BigNat#
+    BigNat#
+  , bigNatAdd
+  , bigNatIsOne
+  , bigNatIsZero
+  , bigNatMul
+  , bigNatRem
+  , bigNatSqr
+  , bigNatSub
+  , bigNatSubUnsafe
+  , oneBigNat
+  , recipModBigNat
+  , shiftLBigNat
+  , shiftRBigNat
+  , testBitBigNat
+  , zeroBigNat
+
+    -- * Integer
+  , Integer(IS, IP, IN)
+  , integerRecipMod
+
+    -- * Conversions
+  , bigNatToInteger
+  , integerToBigNat
+  ) where
+
+#if defined(MIN_VERSION_ghc_bignum)
+import           GHC.Num.BigNat (BigNat#, bigNatAdd, bigNatIsOne, bigNatIsZero, bigNatMul, bigNatRem, bigNatSqr, bigNatSub, bigNatSubUnsafe)
+import qualified GHC.Num.Backend as BN
+import qualified GHC.Num.BigNat as BN
+import           GHC.Num.Integer (Integer(IS, IP, IN))
+import qualified GHC.Num.Integer as Integer
+import           GHC.Exts
+
+-- | Coerce a @BigNat#@ to an integer value.
+bigNatToInteger :: BigNat# -> Integer
+bigNatToInteger = Integer.integerFromBigNat#
+
+-- | @'integerRecipMod' x m@ computes the modular inverse of @x@ mod @m@.
+--
+-- PRECONDITION: @m@ must be strictly positive.
+integerRecipMod :: Integer -> Integer -> Maybe Integer
+integerRecipMod x y =
+  case Integer.integerRecipMod# x (Integer.integerToNaturalClamp y) of
+    (# r | #)  -> Just (toInteger r)
+    (# | () #) -> Nothing
+
+-- | Coerce an integer value to a @BigNat#@.  This operation only really makes
+--   sense for nonnegative values, but this condition is not checked.
+integerToBigNat :: Integer -> BigNat#
+integerToBigNat = Integer.integerToBigNatClamp#
+
+-- Top-level unlifted bindings aren't allowed, so we fake one with a thunk.
+oneBigNat :: (# #) -> BigNat#
+oneBigNat _ = BN.bigNatFromWord# 1##
+
+recipModBigNat :: BigNat# -> BigNat# -> BigNat#
+recipModBigNat = BN.sbignat_recip_mod 0#
+
+shiftLBigNat :: BigNat# -> Int# -> BigNat#
+shiftLBigNat bn i = BN.bigNatShiftL# bn (int2Word# i)
+
+shiftRBigNat :: BigNat# -> Int# -> BigNat#
+shiftRBigNat bn i = BN.bigNatShiftR# bn (int2Word# i)
+
+testBitBigNat :: BigNat# -> Int# -> Bool
+testBitBigNat bn i = isTrue# (BN.bigNatTestBit# bn (int2Word# i))
+
+-- Top-level unlifted bindings aren't allowed, so we fake one with a thunk.
+zeroBigNat :: (# #) -> BigNat#
+zeroBigNat _ = BN.bigNatFromWord# 0##
+#else
+import           GHC.Integer.GMP.Internals (bigNatToInteger, recipModBigNat, shiftLBigNat, shiftRBigNat, testBitBigNat)
+import qualified GHC.Integer.GMP.Internals as GMP
+import           GHC.Exts
+
+type BigNat# = GMP.BigNat
+
+{-# COMPLETE IS, IP, IN #-}
+
+pattern IS :: Int# -> Integer
+pattern IS i = GMP.S# i
+
+pattern IP :: ByteArray# -> Integer
+pattern IP ba = GMP.Jp# (GMP.BN# ba)
+
+pattern IN :: ByteArray# -> Integer
+pattern IN ba = GMP.Jn# (GMP.BN# ba)
+
+bigNatAdd :: BigNat# -> BigNat# -> BigNat#
+bigNatAdd = GMP.plusBigNat
+
+bigNatIsOne :: BigNat# -> Bool
+bigNatIsOne bn = GMP.eqBigNat bn GMP.oneBigNat
+
+bigNatIsZero :: BigNat# -> Bool
+bigNatIsZero = GMP.isZeroBigNat
+
+bigNatMul :: BigNat# -> BigNat# -> BigNat#
+bigNatMul = GMP.timesBigNat
+
+bigNatRem :: BigNat# -> BigNat# -> BigNat#
+bigNatRem = GMP.remBigNat
+
+bigNatSqr :: BigNat# -> BigNat#
+bigNatSqr = GMP.sqrBigNat
+
+bigNatSub :: BigNat# -> BigNat# -> (# (# #) | BigNat# #)
+bigNatSub x y =
+  case GMP.isNullBigNat# res of
+    0# -> (# | res #)
+    _  -> (# (# #) | #)
+  where
+    res = GMP.minusBigNat x y
+
+bigNatSubUnsafe :: BigNat# -> BigNat# -> BigNat#
+bigNatSubUnsafe = GMP.minusBigNat
+
+integerToBigNat :: Integer -> BigNat#
+integerToBigNat (GMP.S# i)  = GMP.wordToBigNat (int2Word# i)
+integerToBigNat (GMP.Jp# b) = b
+integerToBigNat (GMP.Jn# b) = b
+
+-- | @'integerRecipMod' x m@ computes the modular inverse of @x@ mod @m@.
+--
+-- PRECONDITION: @m@ must be strictly positive.
+integerRecipMod :: Integer -> Integer -> Maybe Integer
+integerRecipMod x y
+  | res == 0  = Nothing
+  | otherwise = Just res
+  where
+    res = GMP.recipModInteger x y
+
+oneBigNat :: (##) -> BigNat#
+oneBigNat _ = GMP.oneBigNat
+
+zeroBigNat :: (##) -> BigNat#
+zeroBigNat _ = GMP.zeroBigNat
+#endif