diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,51 @@
+# 3.5.0 -- 2026-01-27
+
+## Administrative changes
+
+* The binary builds are now built with GHC 9.6 rather than 9.4.
+
+## Language changes
+
+* User-defined `newtype` and `enum` types can now derive instances for standard
+  constraints like `Eq` and `Cmp`. This means you can use standard operations
+  like `==` with your custom types. See the [manual
+  section](https://galoisinc.github.io/cryptol/master/OverloadedOperations.html#derived-instances)
+  for more information.
+
+* The built-in types `Option` and `Result` now have derived instances for `Eq`,
+  `Cmp`, and `SignedCmp`.
+
+* We can now infer that `a = Bit`, from the constraint `Integral [n][a]`.
+
+## Bug fixes
+
+* Fix incorrect defaulting during type inference.
+  ([#1957](https://github.com/GaloisInc/cryptol/issues/1957))
+
+* Make comparison operators lazy so that they do not evaluate any more of the
+  data structure than is required to determine the comparison result, matching
+  the behavior of the reference evaluator.
+  ([#1925](https://github.com/GaloisInc/cryptol/issues/1925))
+
+* Modify project loading to update the cache after each module is validated,
+  and make saving the cache atomic on file systems where renaming a file to
+  an existing file is atomic.  This is useful because we get partial results
+  if the validation process is interrupted.
+  
+* Change the default behavior of `-p`/`--project`.  The new behavior is that
+  it will check all files that have changed, and also files that have not
+  been previously verified.  The old behavior would only validate files that
+  have changed since last time.
+
+* Add a new flag, `--modified-project` which gives us the old `-p` behavior
+  (i.e., check only files that have changed).
+
+* Replace the `--untested-project` flag with the `--unsuccessful-project` flag.
+  This will run validation on all files that have not been successfully validated,
+  including ones that perviously failed, and have not changed.
+
+* Allow user to specify how many satisfying results `satProve` (from `IR/Prove.hs`) produces
+
 # 3.4.0 -- 2025-11-07
 
 ## Language changes
@@ -6,7 +54,7 @@
   without an explicit argument, we now run only the properties in the
   currently *focused module*.  This is a change in behavior, because previously
   we used to run all properties in the currently opened *file*.  This change
-  is only noticable when working with nested modules.  The new behavior works
+  is only noticeable when working with nested modules.  The new behavior works
   better when these commands are used from docstrings (e.g., with the
   new behavior, writing `:check` on a submodule, will only check the properties
   in that submodule, as expected).  
@@ -36,7 +84,7 @@
 
 ## Bug fixes
 
-* Fix a discrepency between the behavior of `:check-docstrings` when run
+* Fix a discrepancy between the behavior of `:check-docstrings` when run
   on the REPL vs. when run with a project.
   ([#1903](https://github.com/GaloisInc/cryptol/issues/1903))
 
@@ -289,7 +337,7 @@
 
 * Add `:new-seed` and `:set-seed` commands to the REPL.
   These affect random test generation,
-  and help write reproducable Cryptol scripts.
+  and help write reproducible Cryptol scripts.
 
 * Add support for the CVC5 solver, which can be selected with
   `:set prover=cvc5`. If you want to specify a What4 or SBV backend, you can
@@ -345,7 +393,7 @@
 * "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
+  For example, when matching `{ 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`.
@@ -457,7 +505,7 @@
 ## Language changes
 
 * The `newtype` construct, which has existed in the interpreter in an
-  incomplete and undocumented form for quite a while, is now fullly
+  incomplete and undocumented form for quite a while, is now fully
   supported. The construct is documented in section 1.22 of [Programming
   Cryptol](https://cryptol.net/files/ProgrammingCryptol.pdf). Note,
   however, that the `cryptol-remote-api` RPC server currently does not
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:             3.4.0
+Version:             3.5.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
@@ -29,7 +29,7 @@
   type:     git
   location: https://github.com/GaloisInc/cryptol.git
   -- add a tag on release branches
-  tag: 3.4.0
+  tag: 3.5.0
 
 
 flag static
@@ -174,6 +174,7 @@
                        Cryptol.TypeCheck.Error,
                        Cryptol.TypeCheck.Kind,
                        Cryptol.TypeCheck.Subst,
+                       Cryptol.TypeCheck.Subst.Type,
                        Cryptol.TypeCheck.Instantiate,
                        Cryptol.TypeCheck.Unify,
                        Cryptol.TypeCheck.PP,
diff --git a/cryptol/Main.hs b/cryptol/Main.hs
--- a/cryptol/Main.hs
+++ b/cryptol/Main.hs
@@ -68,7 +68,7 @@
   , optHelp            = False
   , optBatch           = InteractiveRepl
   , optProject         = Nothing
-  , optProjectRefresh  = Project.ModifiedMode
+  , optProjectRefresh  = Project.UntestedMode Project.CachedFailed
   , optCallStacks      = True
   , optCommands        = []
   , optColorMode       = AutoColor
@@ -93,9 +93,12 @@
   , Option "" ["refresh-project"] (NoArg setProjectRefresh)
     "Ignore a pre-existing cache file when loading a project."
 
-  , Option "" ["untested-project"] (NoArg setProjectUntested)
-    "Load all project files that don't have a test result."
+  , Option "" ["unsuccessful-project"] (NoArg setProjectUnsuccessful)
+    "Load all project files that don't have a successful test result."
 
+  , Option "" ["modified-project"] (NoArg setProjectModified)
+    "Load all project files that have been modified."
+
   , Option "e" ["stop-on-error"] (NoArg setStopOnError)
     "stop script execution as soon as an error occurs."
 
@@ -160,8 +163,11 @@
 setProjectRefresh :: OptParser Options
 setProjectRefresh = modify $ \opts -> opts { optProjectRefresh = Project.RefreshMode }
 
-setProjectUntested :: OptParser Options
-setProjectUntested = modify $ \opts -> opts { optProjectRefresh = Project.UntestedMode }
+setProjectUnsuccessful :: OptParser Options
+setProjectUnsuccessful = modify $ \opts -> opts { optProjectRefresh = Project.UntestedMode Project.RecheckFailed }
+
+setProjectModified :: OptParser Options
+setProjectModified = modify $ \opts -> opts { optProjectRefresh = Project.ModifiedMode }
 
 -- | Set the color mode of the terminal output.
 setColorMode :: String -> OptParser Options
diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -642,7 +642,7 @@
  * functions, i.e., functions that are not defined over their entire input
  * range. In these situations, 'None' can be used as a placeholder return value.
  */
-enum Option a = None | Some a
+enum Option a = None | Some a deriving (Eq, Cmp, SignedCmp)
 
 /**
  * Values of the 'Result t e' type can either be 'Ok', representing success and
@@ -651,7 +651,7 @@
  * expected and recoverable. For instance, 'e' might be a 'String' with an error
  * message, or it might be an 'Integer' with an error code.
  */
-enum Result t e = Ok t | Err e
+enum Result t e = Ok t | Err e deriving (Eq, Cmp, SignedCmp)
 
 // Bit specific operations ----------------------------------------
 
diff --git a/src/Cryptol/Eval/FFI.hs b/src/Cryptol/Eval/FFI.hs
--- a/src/Cryptol/Eval/FFI.hs
+++ b/src/Cryptol/Eval/FFI.hs
@@ -20,7 +20,7 @@
 import Cryptol.Eval.FFI.Error ( FFILoadError )
 import Cryptol.Eval (Eval, EvalEnv )
 import Cryptol.TypeCheck.AST
-    ( Name, FFI(..), TVar(TVBound), findForeignDecls )
+    ( FFI(..), TVar(TVBound), findForeignDecls )
 import Cryptol.TypeCheck.FFI.FFIType ( FFIFunType(..) )
 
 #ifdef FFI_ENABLED
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
@@ -31,10 +31,13 @@
 import System.Random.TF.Gen (seedTFGen)
 
 import Data.Bits ((.&.), shiftR)
+import Data.Foldable
 import Data.Maybe (fromMaybe)
 import qualified Data.Map.Strict as Map
 import Data.Map(Map)
+import qualified Data.IntMap.Strict as IMap
 import Data.Ratio ((%))
+import qualified Data.Vector as Vector
 
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,nAdd)
@@ -247,14 +250,21 @@
 
     -- records
     TVRec fs ->
+      doRecord fs
+
+    TVNominal _ _ ntv ->
+      case ntv of
+        -- newtypes
+        TVStruct fs -> doRecord fs
+        _ -> evalPanic "ringBinary" ["Enum/Abstract type not in `Ring`"]
+
+    where
+    doRecord fs =
       do VRecord <$>
             traverseRecordMap
               (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r)))
               fs
 
-    TVNominal {} ->
-      evalPanic "ringBinary" ["Nominal type not in `Ring`"]
-
 type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)
 
 
@@ -326,14 +336,22 @@
 
     -- records
     TVRec fs ->
+      doRecord fs
+
+    TVNominal _ _ ntv ->
+      case ntv of
+        -- newtypes
+        TVStruct fs -> doRecord fs
+        _ -> evalPanic "ringUnary" ["Enum/Abstract type not in `Ring`"]
+
+    where
+    doRecord fs =
       VRecord <$>
         traverseRecordMap
           (\f fty -> sDelay sym (loop' fty (lookupRecord f v)))
           fs
 
-    TVNominal {} -> evalPanic "ringUnary" ["Nominal type not in `Ring`"]
 
-
 {-# SPECIALIZE ringNullary ::
   Concrete ->
   (Integer -> SEval Concrete (SWord Concrete)) ->
@@ -393,12 +411,18 @@
              do xs <- mapM (sDelay sym . loop) tys
                 pure $ VTuple xs
 
-        TVRec fs ->
+        TVRec fs -> doRecord fs
+
+        TVNominal _ _ ntv ->
+          case ntv of
+            TVStruct fs -> doRecord fs
+            _ -> evalPanic "ringNullary" ["Enum/Abstract type not in `Ring`"]
+
+      where
+        doRecord fs =
              do xs <- traverse (sDelay sym . loop) fs
                 pure $ VRecord xs
 
-        TVNominal {} ->
-          evalPanic "ringNullary" ["Nominal type not in `Ring`"]
 
 {-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete ->
       (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
@@ -725,26 +749,30 @@
 
 {-# SPECIALIZE cmpValue ::
   Concrete ->
+  (SBit Concrete -> a -> a -> SEval Concrete a) ->
   (SBit Concrete -> SBit Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (SWord Concrete -> SWord Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (SRational Concrete -> SRational Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (SFloat Concrete -> SFloat Concrete -> SEval Concrete a -> SEval Concrete a) ->
+  (SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (TValue -> GenValue Concrete -> GenValue Concrete -> SEval Concrete a -> SEval Concrete a)
   #-}
 
 cmpValue ::
   Backend sym =>
   sym ->
+  (SBit sym -> a -> a -> SEval sym a) -> -- ^ how to merge @a@s based on a condition
   (SBit sym -> SBit sym -> SEval sym a -> SEval sym a) ->
   (SWord sym -> SWord sym -> SEval sym a -> SEval sym a) ->
   (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
   (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
   (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) ->
   (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) ->
+  (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> -- ^ how to compare enum tags
   (TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a)
-cmpValue sym fb fw fi fz fq ff = cmp
+cmpValue sym merge fb fw fi fz fq ff ftag = cmp
   where
     cmp ty v1 v2 k =
       case ty of
@@ -753,8 +781,8 @@
         TVFloat _ _   -> ff (fromVFloat v1) (fromVFloat v2) k
         TVIntMod n    -> fz n (fromVInteger v1) (fromVInteger v2) k
         TVRational    -> fq (fromVRational v1) (fromVRational v2) k
-        TVArray{}     -> panic "Cryptol.Prims.Value.cmpValue"
-                               [ "Arrays are not comparable" ]
+        TVArray{}     -> evalPanic "Cryptol.Eval.Generic.cmpValue"
+                                   [ "Arrays are not comparable" ]
         TVSeq n t
           | isTBit t  -> do w1 <- fromVWord sym "cmpValue" v1
                             w2 <- fromVWord sym "cmpValue" v2
@@ -763,20 +791,82 @@
                            (enumerateSeqMap n (fromVSeq v1))
                            (enumerateSeqMap n (fromVSeq v2))
                            k
-        TVStream _    -> panic "Cryptol.Prims.Value.cmpValue"
-                                [ "Infinite streams are not comparable" ]
-        TVFun _ _     -> panic "Cryptol.Prims.Value.cmpValue"
-                               [ "Functions are not comparable" ]
+        TVStream _    -> evalPanic "Cryptol.Eval.Generic.cmpValue"
+                                   [ "Infinite streams are not comparable" ]
+        TVFun _ _     -> evalPanic "Cryptol.Eval.Generic.cmpValue"
+                                   [ "Functions are not comparable" ]
         TVTuple tys   -> cmpValues tys (fromVTuple v1) (fromVTuple v2) k
-        TVRec fields  -> cmpValues
-                            (recordElements fields)
-                            (recordElements (fromVRecord v1))
-                            (recordElements (fromVRecord v2))
-                            k
+        TVRec fields  -> cmpRecord fields
 
-        TVNominal {} -> evalPanic "cmpValue"
-                          [ "Nominal type not in `Cmp`" ]
+        TVNominal _ _ ntv ->
+          case ntv of
+            TVStruct fields -> cmpRecord fields
+            TVEnum conTypes -> cmpEnum conTypes
+            TVAbstract -> evalPanic "Cryptol.Eval.Generic.cmpValue"
+                                    [ "Abstract types are not comparable" ]
 
+      where
+        cmpRecord fields = cmpValues
+                             (recordElements fields)
+                             (recordElements (fromVRecord v1))
+                             (recordElements (fromVRecord v2))
+                             k
+
+        cmpEnum conTypes = do
+          let (tag1, cons1) = fromVEnum v1
+              (tag2, cons2) = fromVEnum v2
+          -- first compare based on tag...
+          ftag tag1 tag2
+            -- if both tags are concrete...
+            case (integerAsLit sym tag1, integerAsLit sym tag2) of
+              (Just i, Just j)
+                -- ...then because the comparisons are lazy, this part should
+                -- only be evaluated if tag1 == tag2
+                | i == j -> do
+                  -- in the fully concrete case, just look up the fields for
+                  -- this constructor and compare them
+                  let i' = fromInteger i
+                  case (IMap.lookup i' cons1, IMap.lookup i' cons2) of
+                    (Just con1, Just con2) -> cmpFields i' con1 con2
+                    _ -> evalPanic "Cryptol.Eval.Generic.cmpValue"
+                           ["Missing constructor for tag", show i']
+                | otherwise ->
+                  evalPanic "Cryptol.Eval.Generic.cmpValue"
+                    [ "Concrete enum tags not equal in equal case"
+                    , "Comparisons not lazy enough?" ]
+              _ -> do
+                -- in the symbolic case, here tag1 may or may not equal tag2, so
+                -- we need to explicitly check this
+                sameTag <- intEq sym tag1 tag2
+                -- if tag1 == tag2, then compare by field, otherwise we are done
+                -- comparing
+                mergeEval sym merge sameTag doFields k
+                where
+                  doFields =
+                    -- build up an if-then-else chain for each possible tag
+                    -- value
+                    IMap.foldrWithKey doFieldsForTag notFound $
+                      -- since at this point we know tag1 == tag2, we only need
+                      -- to consider the intersection of their possible
+                      -- constructors
+                      IMap.intersectionWith (,) cons1 cons2
+                  doFieldsForTag i (con1, con2) doRest = do
+                    -- if the tag is i, then compare fields for constructor i
+                    i' <- integerLit sym (toInteger i)
+                    -- we know tag1 == tag2, so we arbitrarily use tag1 here
+                    isThisTag <- intEq sym tag1 i'
+                    mergeEval sym merge isThisTag
+                      (cmpFields i con1 con2)
+                      doRest
+                  notFound = raiseError sym $ NoMatchingConstructor Nothing
+          where
+            cmpFields i con1 con2 =
+              cmpValues
+                (toList (conFields (conTypes Vector.! i)))
+                (toList (conFields con1))
+                (toList (conFields con2))
+                k
+
     cmpValues (t : ts) (x1 : xs1) (x2 : xs2) k =
       do x1' <- x1
          x2' <- x2
@@ -796,7 +886,7 @@
 
 {-# INLINE valEq #-}
 valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
-valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym True)
+valEq sym ty v1 v2 = cmpValue sym (iteBit sym) fb fw fi fz fq ff ftag ty v1 v2 (pure $ bitLit sym True)
   where
   fb x y k   = eqCombine sym (bitEq  sym x y) k
   fw x y k   = eqCombine sym (wordEq sym x y) k
@@ -804,11 +894,12 @@
   fz m x y k = eqCombine sym (znEq sym m x y) k
   fq x y k   = eqCombine sym (rationalEq sym x y) k
   ff x y k   = eqCombine sym (fpEq sym x y) k
+  ftag       = fi
 
 {-# INLINE valLt #-}
 valLt :: Backend sym =>
   sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
-valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)
+valLt sym ty v1 v2 final = cmpValue sym (iteBit sym) fb fw fi fz fq ff ftag ty v1 v2 (pure final)
   where
   fb x y k   = lexCombine sym (bitLessThan  sym x y) (bitEq  sym x y) k
   fw x y k   = lexCombine sym (wordLessThan sym x y) (wordEq sym x y) k
@@ -816,11 +907,12 @@
   fz _ _ _ _ = panic "valLt" ["Z_n is not in `Cmp`"]
   fq x y k   = lexCombine sym (rationalLessThan sym x y) (rationalEq sym x y) k
   ff x y k   = lexCombine sym (fpLessThan   sym x y) (fpEq   sym x y) k
+  ftag       = fi
 
 {-# INLINE valGt #-}
 valGt :: Backend sym =>
   sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
-valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)
+valGt sym ty v1 v2 final = cmpValue sym (iteBit sym) fb fw fi fz fq ff ftag ty v1 v2 (pure final)
   where
   fb x y k   = lexCombine sym (bitGreaterThan  sym x y) (bitEq  sym x y) k
   fw x y k   = lexCombine sym (wordGreaterThan sym x y) (wordEq sym x y) k
@@ -828,6 +920,7 @@
   fz _ _ _ _ = panic "valGt" ["Z_n is not in `Cmp`"]
   fq x y k   = lexCombine sym (rationalGreaterThan sym x y) (rationalEq sym x y) k
   ff x y k   = lexCombine sym (fpGreaterThan   sym x y) (fpEq   sym x y) k
+  ftag       = fi
 
 {-# INLINE eqCombine #-}
 eqCombine :: Backend sym =>
@@ -835,7 +928,12 @@
   SEval sym (SBit sym) ->
   SEval sym (SBit sym) ->
   SEval sym (SBit sym)
-eqCombine sym eq k = join (bitAnd sym <$> eq <*> k)
+eqCombine sym eq k =
+  do e <- eq
+     -- lazy `and` operator
+     case bitAsLit sym e of
+       Just False -> pure e
+       _ -> bitAnd sym e =<< k
 
 {-# INLINE lexCombine #-}
 lexCombine :: Backend sym =>
@@ -846,8 +944,15 @@
   SEval sym (SBit sym)
 lexCombine sym cmp eq k =
   do c <- cmp
-     e <- eq
-     bitOr sym c =<< bitAnd sym e =<< k
+     -- lazy `or` operator
+     case bitAsLit sym c of
+       Just True -> pure c
+       _ ->
+         do e <- eq
+            -- lazy `and` operator
+            case bitAsLit sym e of
+              Just False -> pure c
+              _          -> bitOr sym c =<< bitAnd sym e =<< k
 
 {-# INLINE eqV #-}
 eqV :: Backend sym => sym -> Binary sym
@@ -875,7 +980,8 @@
 
 {-# INLINE signedLessThanV #-}
 signedLessThanV :: Backend sym => sym -> Binary sym
-signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym False)
+signedLessThanV sym ty v1 v2 =
+  VBit <$> cmpValue sym (iteBit sym) fb fw fi fz fq ff ftag ty v1 v2 (pure $ bitLit sym False)
   where
   fb _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on bit type"]
   fw x y k   = lexCombine sym (wordSignedLessThan sym x y) (wordEq sym x y) k
@@ -883,6 +989,7 @@
   fz m _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Z_" ++ show m ++ " type"]
   fq _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Rational type"]
   ff _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Float"]
+  ftag x y k = lexCombine sym (intLessThan sym x y) (intEq sym x y) k
 
 
 
@@ -942,11 +1049,18 @@
 
   -- records
   TVRec fields ->
-      do xs <- traverse (sDelay sym . zeroV sym) fields
-         pure $ VRecord xs
+    doRecord fields
 
-  TVNominal {} -> evalPanic "zeroV" [ "Nominal type not in `Zero`" ]
+  -- newtypes
+  TVNominal _ _ ntv ->
+    case ntv of
+      TVStruct fields -> doRecord fields
+      _ -> evalPanic "zeroV" [ "Enum/Abstract type not in `Zero`" ]
 
+  where
+  doRecord fields =
+      do xs <- traverse (sDelay sym . zeroV sym) fields
+         pure $ VRecord xs
 
 {-# SPECIALIZE joinSeq ::
   Concrete ->
@@ -1289,15 +1403,21 @@
     TVFun _ bty ->
         lam sym $ \ a -> loop' bty (fromVFun sym l a) (fromVFun sym r a)
 
-    TVRec fields ->
+    TVRec fields -> doRecord fields
+
+    TVNominal _ _ ntv ->
+      case ntv of
+        TVStruct fields -> doRecord fields
+        _ -> evalPanic "logicBinary"
+                 [ "Enum/Abstract type not in `Logic`" ]
+
+    where
+    doRecord fields =
       VRecord <$>
         traverseRecordMap
           (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r)))
           fields
 
-    TVNominal {} -> evalPanic "logicBinary"
-                        [ "Nominal type not in `Logic`" ]
-
 {-# SPECIALIZE logicUnary ::
   Concrete ->
   (SBit Concrete -> SEval Concrete (SBit Concrete)) ->
@@ -1346,13 +1466,19 @@
     TVFun _ bty ->
       lam sym $ \ a -> loop' bty (fromVFun sym val a)
 
-    TVRec fields ->
+    TVRec fields -> doRecord fields
+
+    TVNominal _ _ ntv ->
+      case ntv of
+        TVStruct fields -> doRecord fields
+        _ -> evalPanic "logicUnary" [ "Enum/Abstract type not in `Logic`" ]
+
+    where
+    doRecord fields =
       VRecord <$>
         traverseRecordMap
           (\f fty -> sDelay sym (loop' fty (lookupRecord f val)))
           fields
-
-    TVNominal {} -> evalPanic "logicUnary" [ "Nominal type not in `Logic`" ]
 
 
 {-# INLINE assertIndexInBounds #-}
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
@@ -35,6 +35,8 @@
 > import qualified LibBF as FP
 > import qualified GHC.Num.Compat as Integer
 > import qualified Data.List as List
+> import Data.Vector (Vector)
+> import qualified Data.Vector as Vector
 >
 > import Cryptol.ModuleSystem.Name (asPrim,nameIdent)
 > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
@@ -43,7 +45,7 @@
 > import qualified Cryptol.Backend.FloatHelpers as FP
 > import Cryptol.Backend.Monad (EvalError(..))
 > import Cryptol.Eval.Type
->   (TValue(..), TNominalTypeValue(..),
+>   (TValue(..), TNominalTypeValue(..), ConInfo(..),
 >    isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar)
 > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)
 > import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim, unpackIdent)
@@ -1076,9 +1078,9 @@
 a zero value for all the built-in types for Cryptol.
 For bits, bitvectors and the base numeric types, this
 returns the obvious 0 representation.  For sequences, records,
-and tuples, the zero method operates pointwise the underlying types.
-For functions, `zero` returns the constant function that returns
-`zero` in the codomain.
+tuples, and newtypes deriving `Zero`, the zero method operates
+pointwise the underlying types. For functions, `zero` returns
+the constant function that returns `zero` in the codomain.
 
 > zero :: TValue -> Value
 > zero TVBit          = VBit False
@@ -1093,7 +1095,10 @@
 > zero (TVRec fields) = VRecord [ (f, pure (zero fty))
 >                               | (f, fty) <- canonicalFields fields ]
 > zero (TVFun _ bty)  = VFun (\_ -> pure (zero bty))
-> zero (TVNominal {})  = evalPanic "zero" ["Nominal type not in `Zero`"]
+> zero (TVNominal _ _ ntv) =
+>   case ntv of
+>     TVStruct fields -> zero (TVRec fields)
+>     _               -> evalPanic "zero" ["Enum/Abstract type not in `Zero`"]
 
 Literals
 --------
@@ -1162,7 +1167,10 @@
 >         TVArray{}    -> evalPanic "logicUnary" ["Array not in class Logic"]
 >         TVRational   -> evalPanic "logicUnary" ["Rational not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicUnary" ["Float not in class Logic"]
->         TVNominal {}  -> evalPanic "logicUnary" ["Nominal type not in `Logic`"]
+>         TVNominal _ _ ntv ->
+>           case ntv of
+>             TVStruct fields -> go (TVRec fields) val
+>             _ -> evalPanic "logicUnary" ["Enum/Abstract type not in `Logic`"]
 
 > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
 > logicBinary op = go
@@ -1200,7 +1208,10 @@
 >         TVArray{}    -> evalPanic "logicBinary" ["Array not in class Logic"]
 >         TVRational   -> evalPanic "logicBinary" ["Rational not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicBinary" ["Float not in class Logic"]
->         TVNominal {} -> evalPanic "logicBinary" ["Nominal type not in `Logic`"]
+>         TVNominal _ _ ntv ->
+>           case ntv of
+>             TVStruct fields -> go (TVRec fields) l r
+>             _ -> evalPanic "logicBinary" ["Enum/Abstract type not in `Logic`"]
 
 
 Ring Arithmetic
@@ -1224,7 +1235,7 @@
 >     go ty =
 >       case ty of
 >         TVBit ->
->           evalPanic "arithNullary" ["Bit not in class Ring"]
+>           evalPanic "ringNullary" ["Bit not in class Ring"]
 >         TVInteger ->
 >           VInteger <$> i
 >         TVIntMod n ->
@@ -1234,7 +1245,7 @@
 >         TVFloat e p ->
 >           VFloat . fpToBF e p <$> fl e p
 >         TVArray{} ->
->           evalPanic "arithNullary" ["Array not in class Ring"]
+>           evalPanic "ringNullary" ["Array not in class Ring"]
 >         TVSeq w a
 >           | isTBit a  -> vWord w <$> i
 >           | otherwise -> pure $ VList (Nat w) (genericReplicate w (go a))
@@ -1246,8 +1257,10 @@
 >           pure $ VTuple (map go tys)
 >         TVRec fs ->
 >           pure $ VRecord [ (f, go fty) | (f, fty) <- canonicalFields fs ]
->         TVNominal {} ->
->           evalPanic "arithNullary" ["Newtype type not in `Ring`"]
+>         TVNominal _ _ ntv ->
+>           case ntv of
+>             TVStruct fs -> go (TVRec fs)
+>             _ -> evalPanic "ringNullary" ["Enum/Abstract type not in `Ring`"]
 
 > ringUnary ::
 >   (Integer -> E Integer) ->
@@ -1260,11 +1273,11 @@
 >     go ty val =
 >       case ty of
 >         TVBit ->
->           evalPanic "arithUnary" ["Bit not in class Ring"]
+>           evalPanic "ringUnary" ["Bit not in class Ring"]
 >         TVInteger ->
 >           VInteger <$> appOp1 iop (fromVInteger <$> val)
 >         TVArray{} ->
->           evalPanic "arithUnary" ["Array not in class Ring"]
+>           evalPanic "ringUnary" ["Array not in class Ring"]
 >         TVIntMod n ->
 >           VInteger <$> appOp1 (\i -> flip mod n <$> iop i) (fromVInteger <$> val)
 >         TVRational ->
@@ -1284,8 +1297,10 @@
 >           do val' <- val
 >              pure $ VRecord [ (f, go fty (lookupRecord f val'))
 >                             | (f, fty) <- canonicalFields fs ]
->         TVNominal {} ->
->           evalPanic "arithUnary" ["Nominal type not in `Ring`"]
+>         TVNominal _ _ ntv ->
+>           case ntv of
+>             TVStruct fs -> go (TVRec fs) val
+>             _ -> evalPanic "ringUnary" ["Enum/Abstract type not in `Ring`"]
 
 > ringBinary ::
 >   (Integer -> Integer -> E Integer) ->
@@ -1298,7 +1313,7 @@
 >     go ty l r =
 >       case ty of
 >         TVBit ->
->           evalPanic "arithBinary" ["Bit not in class Ring"]
+>           evalPanic "ringBinary" ["Bit not in class Ring"]
 >         TVInteger ->
 >           VInteger <$> appOp2 iop (fromVInteger <$> l) (fromVInteger <$> r)
 >         TVIntMod n ->
@@ -1309,7 +1324,7 @@
 >           VFloat . fpToBF e p <$>
 >             appOp2 (flop e p) (fromVFloat <$> l) (fromVFloat <$> r)
 >         TVArray{} ->
->           evalPanic "arithBinary" ["Array not in class Ring"]
+>           evalPanic "ringBinary" ["Array not in class Ring"]
 >         TVSeq w a
 >           | isTBit a  -> vWord w <$> appOp2 iop (fromVWord =<< l) (fromVWord =<< r)
 >           | otherwise ->
@@ -1332,8 +1347,10 @@
 >              pure $ VRecord
 >                [ (f, go fty (lookupRecord f l') (lookupRecord f r'))
 >                | (f, fty) <- canonicalFields fs ]
->         TVNominal {} ->
->           evalPanic "arithBinary" ["Nominal type not in class `Ring`"]
+>         TVNominal _ _ ntv ->
+>           case ntv of
+>             TVStruct fs -> go (TVRec fs) l r
+>             _ -> evalPanic "ringBinary" ["Enum/Abstract type not in class `Ring`"]
 
 
 Integral
@@ -1463,12 +1480,16 @@
 Comparison
 ----------
 
-Comparison primitives may be applied to any type that is constructed of
-out of base types and tuples, records and finite sequences.
+Comparison primitives may be applied to any type that is constructed
+out of base types and tuples, records, finite sequences, and newtypes
+and enums deriving the appropriate instances.
 All such types are compared using a lexicographic ordering of components.
 On bits, we have `False` < `True`. Sequences and
 tuples are compared left-to-right, and record fields are compared in
-alphabetical order.
+alphabetical order. Newtypes are compared using their underlying records.
+Enums are compared first based on constructor, in the order that they are
+listed in the `enum` declaration, then for enum values with the same
+constructor, by the constructor fields in left-to-right order.
 
 Comparisons on base types are strict in both arguments. Comparisons on
 larger types have short-circuiting behavior: A comparison involving an
@@ -1510,8 +1531,12 @@
 >          ls <- map snd . sortBy (comparing fst) . fromVRecord <$> l
 >          rs <- map snd . sortBy (comparing fst) . fromVRecord <$> r
 >          lexList (zipWith3 lexCompare tys ls rs)
->     TVNominal {} ->
->       evalPanic "lexCompare" ["Nominal type not in `Cmp`"]
+>     TVNominal _ _ ntv ->
+>       case ntv of
+>         TVStruct fields -> lexCompare (TVRec fields) l r
+>         TVEnum conInfos -> lexEnum lexCompare conInfos l r
+>         TVAbstract ->
+>           evalPanic "lexCompare" ["Abstract type not in `Cmp`"]
 >
 > lexList :: [E Ordering] -> E Ordering
 > lexList [] = pure EQ
@@ -1520,6 +1545,29 @@
 >     LT -> pure LT
 >     EQ -> lexList es
 >     GT -> pure GT
+>
+> -- | Lexicographic ordering on enums, given a comparison function for fields.
+> lexEnum :: (TValue -> E Value -> E Value -> E Ordering)
+>         -> Vector (ConInfo TValue) -> E Value -> E Value -> E Ordering
+> lexEnum cmp conInfos l r =
+>   do (lcon, lfields) <- fromVEnum <$> l
+>      (rcon, rfields) <- fromVEnum <$> r
+>      let lconIndex = conIndex lcon
+>          rconIndex = conIndex rcon
+>          -- We arbitrarily use the field types of the left side constructor
+>          -- here, but this is okay since this should only be evaluated when
+>          -- the left and right constructors are the same.
+>          fieldTys = Vector.toList $
+>                       conFields (conInfos Vector.! lconIndex)
+>      lexList (pure (compare lconIndex rconIndex)
+>               : zipWith3 cmp fieldTys lfields rfields)
+>   where
+>     conIndex con =
+>       case Vector.findIndex ((== con) . conIdent) conInfos of
+>         Just i -> i
+>         Nothing ->
+>           evalPanic "lexEnum"
+>             ["Unknown enum constructor " ++ unpackIdent con]
 
 Signed comparisons may be applied to any type made up of non-empty
 bitvectors using finite sequences, tuples and records.
@@ -1564,8 +1612,12 @@
 >          ls <- map snd . sortBy (comparing fst) . fromVRecord <$> l
 >          rs <- map snd . sortBy (comparing fst) . fromVRecord <$> r
 >          lexList (zipWith3 lexSignedCompare tys ls rs)
->     TVNominal {} ->
->       evalPanic "lexSignedCompare" ["Nominal type not in `Cmp`"]
+>     TVNominal _ _ ntv ->
+>       case ntv of
+>         TVStruct fields -> lexSignedCompare (TVRec fields) l r
+>         TVEnum conInfos -> lexEnum lexSignedCompare conInfos l r
+>         TVAbstract ->
+>           evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"]
 
 
 Sequences
diff --git a/src/Cryptol/IR/Prove.hs b/src/Cryptol/IR/Prove.hs
--- a/src/Cryptol/IR/Prove.hs
+++ b/src/Cryptol/IR/Prove.hs
@@ -29,16 +29,17 @@
   [DeclGroup]   {-^ Additional definitions -} ->
   Expr          {-^ The expression we are examining -} ->
   Type          {-^ The type of the expression to examine -} ->
+  Int           {-^ How many satisfying assumptions produced -} ->
   Int           {-^ Timeout in seconds -} ->
   ModuleM [SatResult]
   {- ^ A list of possible models (lazy).  Empty if no models were found. -}
-satProve decls expr exprType timeoutSec =
+satProve decls expr exprType numResults timeoutSec =
   do
     timing <- M.io (newIORef 0)
     let
       cmd =
         ProverCommand {
-          pcQueryType    = SatQuery AllSat,
+          pcQueryType    = SatQuery (SomeSat numResults),
           pcProverName   = "z3",
           pcVerbose      = False,
           pcValidate     = True,
diff --git a/src/Cryptol/IR/TraverseNames.hs b/src/Cryptol/IR/TraverseNames.hs
--- a/src/Cryptol/IR/TraverseNames.hs
+++ b/src/Cryptol/IR/TraverseNames.hs
@@ -214,6 +214,7 @@
       <*> pure (ntKind nt)
       <*> traverseNamesIP (ntConstraints nt)
       <*> traverseNamesIP (ntDef nt)
+      <*> traverse traverseNamesIP (ntDeriving nt)
       <*> pure (ntFixity nt)
       <*> pure (ntDoc nt)
 
diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs
--- a/src/Cryptol/ModuleSystem/Binds.hs
+++ b/src/Cryptol/ModuleSystem/Binds.hs
@@ -31,7 +31,7 @@
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Ident(allNamespaces)
 import Cryptol.Parser.Position
-import Cryptol.Parser.Name(isGeneratedName)
+import Cryptol.Parser.Name(isSystemName)
 import Cryptol.Parser.AST
 import Cryptol.ModuleSystem.Exports(exportedDecls,exported)
 import Cryptol.ModuleSystem.Renamer.Error
@@ -434,7 +434,7 @@
   FreshM m => Namespace -> ModPath -> PName -> Maybe Fixity -> Range -> m Name
 newTop ns m thing fx rng =
   liftSupply (mkDeclared ns m src (getIdent thing) fx rng)
-  where src = if isGeneratedName thing then SystemName else UserName
+  where src = if isSystemName thing then SystemName else UserName
 
 newLocal :: FreshM m => Namespace -> PName -> Range -> m Name
 newLocal ns thing rng = liftSupply (mkLocalPName ns thing rng)
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
@@ -20,8 +20,7 @@
 
 module Cryptol.ModuleSystem.Name (
     -- * Names
-    Name(), NameInfo(..)
-  , NameSource(..)
+    Name(), NameInfo(..), NameSource(..)
   , nameUnique
   , nameIdent
   , mapNameIdent
@@ -74,7 +73,7 @@
 import           Data.Char(isAlpha,toUpper)
 
 
-import           Cryptol.Parser.Name (PName)
+import           Cryptol.Parser.Name (PName, NameSource(..))
 import qualified Cryptol.Parser.Name as PName
 import           Cryptol.Parser.Position (Range,Located(..))
 import           Cryptol.Utils.Fixity
@@ -104,10 +103,6 @@
                  } deriving (Generic, NFData, Show)
 
 
-data NameSource = SystemName | UserName
-                    deriving (Generic, NFData, Show, Eq)
-
-
 instance Eq Name where
   a == b = compare a b == EQ
   a /= b = compare a b /= EQ
@@ -244,22 +239,22 @@
 nameToDefPName :: Name -> PName
 nameToDefPName n =
   case nInfo n of
-    GlobalName _ og -> PName.origNameToDefPName og
-    LocalName _ _ txt -> PName.mkUnqual txt
+    GlobalName ns og -> PName.origNameToDefPName og ns
+    LocalName ns _ txt -> PName.UnQual' txt ns
 
 -- | Compute a `PName` from `Name`, this preserves all qualifiers in the name,
 -- whereas `nameToDefPName` does not.
 nameToPNameWithQualifiers :: Name -> PName
 nameToPNameWithQualifiers n =
   case nameInfo n of
-    GlobalName _ og   -> origNameToPName og
-    LocalName _ _ txt -> PName.mkUnqual txt
+    GlobalName ns og   -> origNameToPName og ns
+    LocalName ns _ txt -> PName.UnQual' txt ns
 
   where
-  origNameToPName :: OrigName -> PName
-  origNameToPName og =
+  origNameToPName :: OrigName -> NameSource -> PName
+  origNameToPName og vis =
     case modPathSplit (ogModule og) of
-      (_top,[] ) -> PName.UnQual ident
+      (_top,[] ) -> PName.UnQual' ident vis
       (_top,ids) -> PName.Qual (packModName (map identText ids)) ident
 
     where
@@ -419,8 +414,8 @@
   where
   ident = PName.getIdent nm
   src   = case nm of
-            PName.NewName {} -> SystemName
-            _                -> UserName
+            PName.NewName {} -> PName.SystemName
+            _                -> PName.UserName
 
 -- | Make a new parameter name.
 mkLocal :: NameSource -> Namespace -> Ident -> Range -> Supply -> (Name,Supply)
@@ -453,7 +448,7 @@
   (u,s') = nextUnique s
   name = Name { nUnique = u
               , nInfo   = GlobalName
-                            UserName
+                            PName.UserName
                             OrigName
                               { ogModule    = own
                               , ogName      = nameIdent n
diff --git a/src/Cryptol/ModuleSystem/Names.hs b/src/Cryptol/ModuleSystem/Names.hs
--- a/src/Cryptol/ModuleSystem/Names.hs
+++ b/src/Cryptol/ModuleSystem/Names.hs
@@ -23,16 +23,20 @@
     One x -> [x]
     Ambig ns -> Set.toList ns
 
+-- | Returns a UserName if one is available, otherwise it returns
+-- | a SystemName.
 anyOne :: Names -> Name
 anyOne xs =
   case xs of
     One x -> x
     Ambig ns
-      |  Set.null ns
-      -> panic "anyOne" ["Ambig with no names"]
-      |  otherwise
-      -> Set.elemAt 0 ns
-
+      | Set.null ns ->
+          panic "anyOne" ["Ambig with no names"]
+      | Set.null l -> Set.elemAt 0 ns
+      | otherwise -> Set.elemAt 0 l
+      where
+        l = Set.filter (\x -> nameSrc x == UserName) ns
+        
 instance Semigroup Names where
   xs <> ys =
     case (xs,ys) of
@@ -93,4 +97,3 @@
       ys = case y of
              One z    -> Set.delete z xs
              Ambig zs -> Set.difference xs zs
-
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
@@ -176,7 +176,7 @@
 qualify pfx (NamingEnv env) = NamingEnv (Map.mapKeys toQual <$> env)
   where
   toQual (Qual mn n) = Qual (prependChunks pfx' mn) n
-  toQual (UnQual n)  = Qual pfx n
+  toQual (UnQual' n _ns)  = Qual pfx n
   toQual n@NewName{} = n
 
   -- | prependChunks - add ChunksText to start of ModName
@@ -214,14 +214,20 @@
   NamingEnv ns = consToValues env
 
 -- | Get the subset of the first environment that shadows something
--- in the second one.
-findShadowing :: NamingEnv -> NamingEnv -> [ (PName,Name,[Name]) ]
-findShadowing (NamingEnv lhs) rhs =
-  [ (p, anyOne xs, namesToList ys)
-  | (ns,mp) <- Map.toList lhs
-  , (p,xs) <- Map.toList mp
-  , Just ys <- [ lookupNS ns p rhs ]
-  ]
+-- in the second one. We only consider UserNames in the second enviornment.
+findShadowing :: NamingEnv -> NamingEnv -> [(PName, Name, [Name])]
+findShadowing (NamingEnv lhs) rhs = res
+  where
+    res =
+      [ (p, x, ysList)
+        | (ns, mp) <- Map.toList lhs,
+          (p, xs) <- Map.toList mp,
+          let x = anyOne xs,
+          Just ys <- [lookupNS ns p rhs],
+          let ysList = filter isUser (namesToList ys),
+          not (null ysList)
+      ]
+    isUser z = nameSrc z == UserName
 
 -- | Do an arbitrary choice for ambiguous names.
 -- We do this to continue checking afetr we've reported an ambiguity error.
@@ -255,7 +261,7 @@
                                map fromTy (Map.elems mpnTypes))
     ]
   where
-  toPName n = mkUnqual (nameIdent n)
+  toPName n = UnQual' (nameIdent n) (nameSrc n)
 
   fromTy tp = let nm = T.mtpName tp
               in (toPName nm, One nm)
@@ -276,7 +282,7 @@
 unqualifiedEnv IfaceDecls { .. } =
   mconcat [ exprs, tySyns, ntTypes, ntExprs, mods, sigs ]
   where
-  toPName n = mkUnqual (nameIdent n)
+  toPName n = UnQual' (nameIdent n) (nameSrc n)
 
   exprs   = mconcat [ singletonNS NSValue (toPName n) n
                     | n <- Map.keys ifDecls ]
diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -876,12 +876,14 @@
        depsOf (NamedThing nameC) (addDep (thing nameT))
 
        depsOf (NamedThing (thing nameT)) $
-         do ps'   <- traverse rename (nParams n)
-            body' <- traverse (traverse rename) (nBody n)
+         do ps'       <- traverse rename (nParams n)
+            body'     <- traverse (traverse rename) (nBody n)
+            deriving' <- traverse (rnLocated (renameType NameUse)) (nDeriving n)
             return Newtype { nName   = nameT
                            , nConName = nameC
                            , nParams = ps'
-                           , nBody   = body' }
+                           , nBody   = body'
+                           , nDeriving = deriving' }
 
 instance Rename EnumDecl where
   rename n =
@@ -898,9 +900,11 @@
                      do ts' <- traverse rename (ecFields (tlValue tlEc))
                         let con = EnumCon { ecName = c, ecFields = ts' }
                         pure tlEc { tlValue = con }
+            deriving' <- traverse (rnLocated (renameType NameUse)) (eDeriving n)
             pure EnumDecl { eName = nameT
                           , eParams = ps'
                           , eCons = cons
+                          , eDeriving = deriving'
                           }
 
 -- | Try to resolve a name.
@@ -1120,7 +1124,7 @@
                  UpdFun -> UpdField UpdFun [l] <$>
                                         rename (EFun emptyFunDesc [PVar p] e)
                        where
-                       p = UnQual . selName <$> last ls
+                       p = mkUnqual . selName <$> last ls           
          _ -> UpdField UpdFun [l] <$> rename (EUpd Nothing [ UpdField h more e])
       [] -> panic "rename@UpdField" [ "Empty label list." ]
 
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
@@ -350,11 +350,14 @@
                 pure (forceUnambig env)
 
 -- | Issue warnings if entries in the first environment would
--- shadow something in the second.
+--   shadow something in the second. This warning is only emited
+--   for UserNames
 checkShadowing :: NamingEnv -> NamingEnv -> RenameM ()
 checkShadowing envNew envOld =
-  mapM_ recordWarning
-    [ SymbolShadowed p x xs | (p,x,xs) <- findShadowing envNew envOld ]
+  mapM_
+    recordWarning
+    [ SymbolShadowed p x xs | (p, x, xs) <- findShadowing envNew envOld
+    ]
 
 
 -- | Shadow the current naming environment with some more names.
diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y
--- a/src/Cryptol/Parser.y
+++ b/src/Cryptol/Parser.y
@@ -9,6 +9,8 @@
 
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE PatternSynonyms #-}
+
 module Cryptol.Parser
   ( parseModule
   , parseProgram, parseProgramWith
@@ -39,6 +41,7 @@
 import Cryptol.Parser.Token
 import Cryptol.Parser.ParserUtils
 import Cryptol.Parser.Unlit(PreProc(..), guessPreProc)
+import Cryptol.Parser.Name (mkUnqual, pattern UnQual)
 import Cryptol.Utils.RecordMap(RecordMap)
 
 import Paths_cryptol
@@ -69,6 +72,7 @@
   'type'      { Located $$ (Token (KW KW_type   ) _)}
   'newtype'   { Located $$ (Token (KW KW_newtype) _)}
   'enum'      { Located $$ (Token (KW KW_enum) _)}
+  'deriving'  { Located $$ (Token (KW KW_deriving) _)}
   'module'    { Located $$ (Token (KW KW_module ) _)}
   'submodule' { Located $$ (Token (KW KW_submodule ) _)}
   'where'     { Located $$ (Token (KW KW_where  ) _)}
@@ -442,16 +446,16 @@
   : type                              {% mkPropGuards $1 }
 
 
-newtype                            :: { Newtype PName }
-  : 'newtype' type '=' newtype_body   {% mkNewtype $2 $4 }
+newtype                                   :: { Newtype PName }
+  : 'newtype' type '=' newtype_body deriving {% mkNewtype $2 $4 $5 }
 
 newtype_body            :: { Located (RecordMap Ident (Range, Type PName)) }
   : '{' '}'                {% mkRecord (rComb $1 $2) (Located emptyRange) [] }
   | '{' field_types '}'    {% mkRecord (rComb $1 $3) (Located emptyRange) $2 }
 
 
-enum                              :: { EnumDecl PName }
-  : 'enum' type '=' enum_body        {% mkEnumDecl $2 $4 }
+enum                                :: { EnumDecl PName }
+  : 'enum' type '=' enum_body deriving {% mkEnumDecl $2 $4 $5 }
 
 enum_body                         :: { [TopLevel (EnumCon PName)] }
   :     enum_con                     { [$1] }
@@ -461,6 +465,10 @@
 enum_con                           :: { TopLevel (EnumCon PName) }
   : app_type                          {% mkConDecl Nothing   Public $1 }
   | doc  app_type                     {% mkConDecl (Just $1) Public $2 }
+
+deriving                       :: { [Located PName] }
+  : 'deriving' '(' vars_comma ')' { reverse $3 }
+  | {- empty -}                   { [] }
 
 vars_comma                 :: { [ LPName ]  }
   : var                       { [ $1]      }
diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs
--- a/src/Cryptol/Parser/AST.hs
+++ b/src/Cryptol/Parser/AST.hs
@@ -154,7 +154,7 @@
 newtype Program name = Program [TopDecl name]
                        deriving (Show)
 
-{- | A module for the pre-typechecker phasese. The two parameters are:
+{- | A module for the pre-typechecker phases. The two parameters are:
 
   * @mname@ the type of module names. This is because top-level and nested
     modules use different types to identify a module.
@@ -176,7 +176,7 @@
   } deriving (Show, Generic, NFData)
 
 
--- | Different flavours of module we have.
+-- | Different flavours of modules we have.
 data ModuleDefinition name =
     NormalModule [TopDecl name]
 
@@ -587,12 +587,14 @@
   , nParams   :: [TParam name]       -- ^ Type params
   , nConName  :: !name               -- ^ Constructor function name
   , nBody     :: Rec (Type name)     -- ^ Body
+  , nDeriving :: [Located name]      -- ^ Derived typeclasses
   } deriving (Eq, Show, Generic, NFData)
 
 data EnumDecl name = EnumDecl
   { eName     :: Located name               -- ^ Type name
   , eParams   :: [TParam name]              -- ^ Type params
   , eCons     :: [TopLevel (EnumCon name)]  -- ^ Value constructors
+  , eDeriving :: [Located name]             -- ^ Derived typeclasses
   } deriving (Show, Generic, NFData)
 
 data EnumCon name = EnumCon
@@ -1631,12 +1633,14 @@
                     , nParams   = nParams n
                     , nConName  = nConName n
                     , nBody     = fmap noPos (nBody n)
+                    , nDeriving = map noPos (nDeriving n)
                     }
 
 instance NoPos (EnumDecl name) where
   noPos n = EnumDecl { eName    = noPos (eName n)
                      , eParams  = eParams n
                      , eCons    = map noPos (eCons n)
+                     , eDeriving = map noPos (eDeriving n)
                      }
 
 instance NoPos (EnumCon name) where
diff --git a/src/Cryptol/Parser/AST/Builder.hs b/src/Cryptol/Parser/AST/Builder.hs
--- a/src/Cryptol/Parser/AST/Builder.hs
+++ b/src/Cryptol/Parser/AST/Builder.hs
@@ -58,6 +58,8 @@
 funT2 f a b = var f $^ [PosInst a, PosInst b]
 
 -- | Create an unqualified variable expression from an identifier.
+--   We assume here that the variable's PName is user visible, i.e. 
+--   is a UserName
 var :: Ident -> Expr PName
 var = EVar . mkUnqual
 
diff --git a/src/Cryptol/Parser/ExpandPropGuards.hs b/src/Cryptol/Parser/ExpandPropGuards.hs
--- a/src/Cryptol/Parser/ExpandPropGuards.hs
+++ b/src/Cryptol/Parser/ExpandPropGuards.hs
@@ -27,6 +27,7 @@
 import Data.Foldable (traverse_)
 import Data.Text (pack)
 import GHC.Generics (Generic)
+import Cryptol.Parser.Name (NameSource(SystemName))
 
 -- | Monad
 type ExpandPropGuardsM a = Either Error a
@@ -282,10 +283,10 @@
       let txt = identText ident
           txt' = pack $ show $ pp props
        in Qual modName (mkIdent $ txt <> txt') <$ locName
-    UnQual ident ->
+    UnQual' ident _ns ->
       let txt = identText ident
           txt' = pack $ show $ pp props
-       in UnQual (mkIdent $ txt <> txt') <$ locName
+       in UnQual' (mkIdent $ txt <> txt') SystemName <$ locName
     NewName _ _ ->
       panic "mkName"
         [ "During expanding prop guards"
diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x
--- a/src/Cryptol/Parser/Lexer.x
+++ b/src/Cryptol/Parser/Lexer.x
@@ -108,6 +108,7 @@
 "interface"               { emit $ KW KW_interface }
 "newtype"                 { emit $ KW KW_newtype }
 "enum"                    { emit $ KW KW_enum }
+"deriving"                { emit $ KW KW_deriving }
 "pragma"                  { emit $ KW KW_pragma }
 "property"                { emit $ KW KW_property }
 "then"                    { emit $ KW KW_then }
diff --git a/src/Cryptol/Parser/Name.hs b/src/Cryptol/Parser/Name.hs
--- a/src/Cryptol/Parser/Name.hs
+++ b/src/Cryptol/Parser/Name.hs
@@ -8,8 +8,21 @@
 
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE PatternSynonyms #-}
 
-module Cryptol.Parser.Name where
+module Cryptol.Parser.Name (
+  NameSource(..)
+  , PName(..)
+  , Pass(..)
+  , mkQual
+  , mkUnqual
+  , mkUnqualSystem
+  , origNameToDefPName
+  , getModName
+  , getIdent
+  , isSystemName
+  , pattern UnQual
+  ) where
 
 import Cryptol.Utils.Fixity
 import Cryptol.Utils.Ident
@@ -22,8 +35,15 @@
 
 -- Names -----------------------------------------------------------------------
 
+data NameSource = SystemName | UserName
+                    deriving (Generic, Show, Ord, Eq)
 -- | Names that originate in the parser.
-data PName = UnQual !Ident
+--   Note here that other kinds of PName do not need this kind of flag because: 
+--   (1) NewName are generated by the system, so these should never be user visible.
+--   (2) Qual names are user names use to refer to imported modules. Should these names
+--       names ever be used to refer to system names, then there make be a bug in the renamer
+--       that needs to be fixed.
+data PName = UnQual' !Ident !NameSource
              -- ^ Unqualified names like @x@, @Foo@, or @+@.
            | Qual !ModName !Ident
              -- ^ Qualified names like @Foo::bar@ or @module::!@.
@@ -39,22 +59,31 @@
 
 instance NFData PName
 instance NFData Pass
+instance NFData NameSource
 
+-- | Pattern synonym for when we are trying to deconstruct
+--   unqualified PNames to get their identifiers.
+pattern UnQual :: Ident -> PName
+pattern UnQual i <- UnQual' i _
+
 mkUnqual :: Ident -> PName
-mkUnqual  = UnQual
+mkUnqual  = (`UnQual'` UserName)
 
+mkUnqualSystem :: Ident -> PName
+mkUnqualSystem = (`UnQual'` SystemName)
+
 mkQual :: ModName -> Ident -> PName
 mkQual  = Qual
 
 -- | Compute a `PName` for the definition site corresponding to the given
 -- `OrigName`.   Usually this is an unqualified name, but names that come
 -- from module parameters are qualified with the corresponding parameter name.
-origNameToDefPName :: OrigName -> PName
-origNameToDefPName og = toPName (ogName og)
+origNameToDefPName :: OrigName -> NameSource -> PName
+origNameToDefPName og vis = toPName (ogName og)
   where
   toPName =
     case ogFromParam og of
-      Nothing -> UnQual
+      Nothing -> (`UnQual'` vis)
       Just sig -> Qual (identToModName sig)
 
 getModName :: PName -> Maybe ModName
@@ -62,7 +91,7 @@
 getModName _           = Nothing
 
 getIdent :: PName -> Ident
-getIdent (UnQual n)    = n
+getIdent (UnQual' n _)    = n
 getIdent (Qual _ n)    = n
 getIdent (NewName p i) = packIdent ("__" ++ pass ++ show i)
   where
@@ -71,11 +100,16 @@
            MonoValues         -> "mv"
            ExpandPropGuards _ -> "epg"
 
-isGeneratedName :: PName -> Bool
-isGeneratedName x =
+
+
+isSystemName :: PName -> Bool
+isSystemName x =
   case x of
-    NewName {} -> True
-    _          -> False
+    UnQual' _id ns ->   case ns of
+                          SystemName -> True
+                          UserName -> False
+    Qual _md _id -> False
+    NewName _p _i -> True
 
 instance PP PName where
   ppPrec _ = ppPrefixName
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
@@ -12,6 +12,7 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE LambdaCase #-}
@@ -55,6 +56,7 @@
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic
 import Cryptol.Utils.RecordMap
+import Cryptol.Parser.Name (pattern UnQual, mkUnqualSystem)
 
 
 parseString :: Config -> ParseM a -> String -> Either ParseError a
@@ -195,14 +197,6 @@
 expected x = P $ \cfg _ s ->
                     Left (HappyUnexpected (cfgSource cfg) (sPrevTok s) x)
 
-
-
-
-
-
-
-
-
 mkModName :: [Text] -> ModName
 mkModName = packModName
 
@@ -222,7 +216,7 @@
                                $ modNameToNormalModName t
         ImpNested nm ->
           case nm of
-            UnQual i -> i
+            UnQual' i _ -> i
             Qual _ i -> i
             NewName {} -> panic "mkModParamName" ["Unexpected NewName",show lsig]
     Just m -> packIdent (last (modNameChunks (thing m)))
@@ -599,7 +593,6 @@
 mkTypeInst x | nullIdent (thing (name x)) = PosInst (value x)
              | otherwise                  = NamedInst x
 
-
 mkTParam :: Located Ident -> Maybe Kind -> ParseM (TParam PName)
 mkTParam Located { srcRange = rng, thing = n } k
   | n == widthIdent = errorMessage rng ["`width` is not a valid type parameter name."]
@@ -620,24 +613,27 @@
 mkNewtype ::
   Type PName ->
   Located (RecordMap Ident (Range, Type PName)) ->
+  [Located PName] ->
   ParseM (Newtype PName)
-mkNewtype thead def =
+mkNewtype thead def derivs =
   do (nm,params) <- typeToDecl thead
-     pure (Newtype nm params (thing nm) (thing def))
+     pure (Newtype nm params (thing nm) (thing def) derivs)
 
 mkEnumDecl ::
   Type PName ->
   [ TopLevel (EnumCon PName) ] {- ^ Reversed -} ->
+  [Located PName] ->
   ParseM (EnumDecl PName)
-mkEnumDecl thead def =
+mkEnumDecl thead def derivs =
   do (nm,params) <- typeToDecl thead
      mapM_ reportRepeated
         (Map.toList (Map.fromListWith (++) [ (thing k,[srcRange k])
                                            | k <- map (ecName . tlValue) def ]))
      pure EnumDecl
-            { eName   = nm
-            , eParams = params
-            , eCons   = reverse def
+            { eName     = nm
+            , eParams   = params
+            , eCons     = reverse def
+            , eDeriving = derivs
             }
   where
   reportRepeated (i,xs) =
@@ -650,6 +646,7 @@
 
       _ -> pure ()
 
+-- | This function handles constructor declarations
 mkConDecl ::
   Maybe (Located Text) -> ExportType ->
   Type PName -> ParseM (TopLevel (EnumCon PName))
@@ -662,9 +659,9 @@
       TLocated t1 r -> go (Just r) t1
       TUser n ts ->
         case thing n of
-          UnQual i
+          UnQual' i ns 
             | isUpperIdent i ->
-              pure EnumCon { ecName = Located (srcRange n) (UnQual i)
+              pure EnumCon { ecName = Located (srcRange n) (UnQual' i ns)
                            , ecFields = ts
                            }
             | otherwise ->
@@ -1135,6 +1132,7 @@
                         , mDocTop = Nothing
                         }
 
+-- | Make a nested module, i.e. when you have a module inside a module.
 mkNested :: Module PName -> ParseM (NestedModule PName)
 mkNested m =
   case modNameChunks (thing nm) of
@@ -1415,8 +1413,11 @@
                     AnonIfaceMod -> modNameIfaceMod
   toImpName     = ImpTop
 
+-- | Make anonymous names, i.e. a thing without a user visible name.
+--   Anonymous names are used when we desugar some things related to the module system  
+--   (e.g. parameter blocks become interface modules).
 instance MkAnon PName where
-  mkAnon what   = mkUnqual
+  mkAnon what   = mkUnqualSystem
                 . case what of
                     AnonArg l c  -> const (identAnonArg l c)
                     AnonIfaceMod -> identAnonIfaceMod
@@ -1564,7 +1565,7 @@
   origMod = iModule (thing i)
 
   iname = Located {
-    thing =mkUnqual
+    thing = mkUnqualSystem
         $ let pos = from (srcRange i)
           in identAnonInstImport (line pos) (col pos),
     srcRange = srcRange origMod
@@ -1580,6 +1581,5 @@
                        , tlDoc    = Nothing
                        , tlValue  = NestedModule m
                        }
-
 
 
diff --git a/src/Cryptol/Parser/Token.hs b/src/Cryptol/Parser/Token.hs
--- a/src/Cryptol/Parser/Token.hs
+++ b/src/Cryptol/Parser/Token.hs
@@ -37,6 +37,7 @@
               | KW_submodule
               | KW_newtype
               | KW_enum
+              | KW_deriving
               | KW_pragma
               | KW_property
               | KW_then
diff --git a/src/Cryptol/Project.hs b/src/Cryptol/Project.hs
--- a/src/Cryptol/Project.hs
+++ b/src/Cryptol/Project.hs
@@ -8,6 +8,7 @@
   , ChangeStatus(..)
   , InvalidStatus(..)
   , LoadProjectMode(..)
+  , CheckFailedMode(..)
   , Parsed
   , loadProject
   , depMap
@@ -46,12 +47,22 @@
           untested (InFile f) =
             case out of
               Left _ -> True
-              Right m -> Map.lookup (CacheInFile f) m /= Just (Just True)
+              Right m ->
+                case mode of
+                  UntestedMode checkFailed ->
+                    case Map.lookup (CacheInFile f) m of
+                       Nothing            -> True
+                       Just Nothing       -> True
+                       Just (Just True)   -> False
+                       Just (Just False)  ->
+                         case checkFailed of
+                           RecheckFailed -> True
+                           CachedFailed  -> False
+                  RefreshMode  -> True
+                  ModifiedMode -> False
 
-      let needLoad = case mode of
-            RefreshMode  -> [thing (P.mName m) | Scanned _ _ ps <- Map.elems statuses, (m, _) <- ps]
-            ModifiedMode -> [thing (P.mName m) | Scanned Changed _ ps <- Map.elems statuses, (m, _) <- ps]
-            UntestedMode -> [thing (P.mName m) | (k, Scanned ch _ ps) <- Map.assocs statuses, ch == Changed || untested k,  (m, _) <- ps]
+      let needLoad =
+            [thing (P.mName m) | (k, Scanned ch _ ps) <- Map.assocs statuses, ch == Changed || untested k, (m, _) <- ps]
       let order = loadOrder deps needLoad
 
       let modDetails = Map.fromList [(thing (P.mName m), (m, mp, fp)) | (mp, Scanned _ fp ps) <- Map.assocs statuses, (m, _) <- ps]
diff --git a/src/Cryptol/Project/Cache.hs b/src/Cryptol/Project/Cache.hs
--- a/src/Cryptol/Project/Cache.hs
+++ b/src/Cryptol/Project/Cache.hs
@@ -9,6 +9,7 @@
 import qualified Data.ByteString                  as BS
 import           Data.Set                         (Set)
 import           System.Directory
+import           System.IO
 import           System.FilePath                  as FP
 import           System.IO.Error
 import qualified Toml
@@ -102,7 +103,11 @@
 
 data CacheEntry = CacheEntry
   { cacheFingerprint :: FullFingerprint
+    -- ^ Identifier for a module that is part of the project
+
   , cacheDocstringResult :: Maybe Bool
+    -- ^ `Nothing` means unchecked,
+    -- `Just` means checked, and if validation succeeded.
   }
   deriving (Show, Read)
 
@@ -126,7 +131,7 @@
 emptyLoadCache :: LoadCache
 emptyLoadCache = LoadCache { cacheModules = mempty }
 
--- | Load a cache.  Also returns an id for the cahce.
+-- | Load a cache.  Also returns an id for the cache.
 -- If there is no cache (or it failed to load), then we return an empty id.
 loadLoadCache :: IO (LoadCache, CacheId)
 loadLoadCache =
@@ -144,5 +149,8 @@
   do createDirectoryIfMissing False metaDir
      let txt = Text.pack (show (Toml.encode cache))
          !bytes = Text.encodeUtf8 txt
-     BS.writeFile loadCachePath bytes
+     (tmpFile,h) <- openBinaryTempFile metaDir "load-cache-XXXXX.toml"
+     BS.hPut h bytes
+     hClose h
+     renameFile tmpFile loadCachePath
      pure (SHA256.hash bytes)
diff --git a/src/Cryptol/Project/Config.hs b/src/Cryptol/Project/Config.hs
--- a/src/Cryptol/Project/Config.hs
+++ b/src/Cryptol/Project/Config.hs
@@ -22,9 +22,17 @@
   } deriving Show
 
 data LoadProjectMode
-  = RefreshMode  -- load all files
-  | ModifiedMode -- load modified files
-  | UntestedMode -- load files without a successful test result
+  = RefreshMode 
+    -- ^ load all files
+  | ModifiedMode
+    -- ^ load modified files
+  | UntestedMode CheckFailedMode
+    -- ^ load files without a successful test result
+  deriving Show
+
+-- | Indicates if we should load files that have not changed, but
+-- contain failed properties.
+data CheckFailedMode = RecheckFailed | CachedFailed
   deriving Show
 
 instance FromValue Config where
diff --git a/src/Cryptol/Project/Monad.hs b/src/Cryptol/Project/Monad.hs
--- a/src/Cryptol/Project/Monad.hs
+++ b/src/Cryptol/Project/Monad.hs
@@ -148,7 +148,7 @@
             (cache,cacheId) <-
               case mode of
                 RefreshMode  -> pure (emptyLoadCache, emptyCacheId)
-                UntestedMode -> loadLoadCache
+                UntestedMode _ -> loadLoadCache
                 ModifiedMode -> loadLoadCache
             pure LoadConfig { canonRoot = path
                             , loadCache = cache
diff --git a/src/Cryptol/REPL/Browse.hs b/src/Cryptol/REPL/Browse.hs
--- a/src/Cryptol/REPL/Browse.hs
+++ b/src/Cryptol/REPL/Browse.hs
@@ -6,8 +6,6 @@
 import qualified Data.Map as Map
 import Data.Maybe(mapMaybe)
 import Data.List(sortBy)
-import Data.Void (Void)
-import qualified Prettyprinter as PP
 
 import Cryptol.Parser.AST(Pragma(..))
 import qualified Cryptol.TypeCheck.Type as T
@@ -38,7 +36,7 @@
     ]
 
   disp     = DispInfo { dispHow = how, env = mctxNameDisp mc }
-  decls    = filterIfaceDecls (`Set.member` visNames) (mctxDecls mc)
+  decls    = filterIfaceDecls (`Set.member` visUserNames) (mctxDecls mc)
   allNames = namingEnvNames (mctxNames mc)
   notAnon nm = identIsNormal (nameIdent nm) &&
                case nameModPathMaybe nm of
@@ -48,6 +46,7 @@
              case how of
                BrowseInScope  -> allNames
                BrowseExported -> mctxExported mc
+  visUserNames = Set.filter (\n -> nameSrc n == UserName) visNames
 
 data DispInfo = DispInfo { dispHow :: BrowseHow, env :: NameDisp }
 
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
@@ -112,6 +112,7 @@
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.RecordMap
 import qualified Cryptol.Parser.AST as P
+import           Cryptol.Parser.Name (mkUnqual)
 import qualified Cryptol.Project as Proj
 import qualified Cryptol.Transform.Specialize as S
 import Cryptol.Symbolic
@@ -1845,7 +1846,7 @@
                     }
   liftModuleCmd (M.evalDecls [T.NonRecursive decl])
   denv <- getDynEnv
-  let nenv' = M.singletonNS M.NSValue (P.UnQual itIdent) freshIt
+  let nenv' = M.singletonNS M.NSValue (mkUnqual itIdent) freshIt
                            `M.shadowing` M.deNames denv
   setDynEnv $ denv { M.deNames = nenv' }
   return freshIt
@@ -2285,7 +2286,7 @@
 checkDocStringsCmd ::
   String {- ^ module name -} ->
   REPL CommandResult
-checkDocStringsCmd input = withModule input (checkModName 0)
+checkDocStringsCmd input = withModule input (fmap snd . checkModName Nothing 0)
 
 
 countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int)
@@ -2299,39 +2300,39 @@
       | crSuccess (srResult result) = (successes + 1, nofences, failures)
       | otherwise = (successes, nofences, failures + 1)
 
-withValidModule :: P.ModName -> String -> (M.LoadedModule -> REPL CommandResult) -> REPL CommandResult
-withValidModule mn tab f =
+withValidModule :: P.ModName -> String -> (CommandResult -> REPL a) -> (M.LoadedModule -> REPL a) -> REPL a
+withValidModule mn tab kNo kYes =
  do env <- getModuleEnv
     case M.lookupModule mn env of
       Nothing ->
         case M.lookupSignature mn env of
           Nothing ->
            do rPutStrLn (tab ++ "Module " ++ show mn ++ " is not loaded")
-              pure emptyCommandResult { crSuccess = False }
+              kNo emptyCommandResult { crSuccess = False }
           Just{} ->
            do rPutStrLn (tab ++ "Skipping docstrings on interface module")
-              pure emptyCommandResult
+              kNo emptyCommandResult
       Just fe
         | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do
           rPutStrLn (tab ++ "Skipping docstrings on parameterized module")
-          pure emptyCommandResult
-        | otherwise -> f fe
+          kNo emptyCommandResult
+        | otherwise -> kYes fe
 
 
-checkModName :: Int -> P.ModName -> REPL CommandResult
-checkModName ind mn =
-  withValidModule mn tab (\m -> do
-              (results,_) <- checkDocStrings m Nothing
+checkModName :: Maybe Proj.CacheId -> Int -> P.ModName -> REPL (Maybe Proj.CacheId, CommandResult)
+checkModName mbCid ind mn =
+  withValidModule mn tab (\r -> pure (mbCid,r)) (\m -> do
+              (results,newCid) <- checkDocStrings m mbCid
               let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results]
               rPutStrLn ("Successes: " ++ show successes ++
                           ", No fences: " ++ show nofences ++
                           ", Failures: " ++ show failures)
-              pure emptyCommandResult { crSuccess = failures == 0 })
+              pure (Just newCid, emptyCommandResult { crSuccess = failures == 0 }))
   where tab = replicate ind ' '
 
 checkModNameForPrint :: P.ModName -> REPL CommandResult
 checkModNameForPrint mn =
-  withValidModule mn "" (\m -> do
+  withValidModule mn "" pure (\m -> do
                             printDocStrings m
                             pure emptyCommandResult { crSuccess = True })
 
@@ -2352,48 +2353,12 @@
       Right ((fps, mp, docstringResults),env) ->
        do setModuleEnv env
           let cache0 = fmap (\fp -> Proj.CacheEntry { cacheDocstringResult = Nothing, cacheFingerprint = fp }) fps
-          (cache, success) <-
-            foldM (\(fpAcc_, success_) (k, v) ->
-              case k of
-                M.InMem{} -> pure (fpAcc_, success_)
-                M.InFile path ->
-                  case v of
-                    Proj.Invalid e ->
-                     do rPrint ("Failed to process module:" <+> (text path <> ":") $$
-                                 indent 2 (ppInvalidStatus e))
-                        pure (fpAcc_, False) -- report failure
-                    Proj.Scanned Proj.Unchanged _ ms ->
-                      foldM f (fpAcc_, success_) ms
-                      where
-                        f (fpAcc, success) (m, _) =
-                         do let name = P.thing (P.mName m)
-                            case join (Map.lookup (Proj.CacheInFile path) docstringResults) of
-                              Just True  ->
-                               do rPrint ("Checking module" <+> hcat [pp name, ": PASS (cached)"])
-                                  let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just True }) (Proj.CacheInFile path) fpAcc
-                                  pure (fpAcc', success) -- preserve success
-
-                              Just False ->
-                               do rPrint ("Checking module" <+> hcat [pp name, ": FAIL (cached)"])
-                                  let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just False }) (Proj.CacheInFile path) fpAcc
-                                  pure (fpAcc', False) -- preserve failure
-
-                              Nothing ->
-                               do checkRes <- checkModName 2 name
-                                  let success1 = crSuccess checkRes
-                                  let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just success1 }) (Proj.CacheInFile path) fpAcc
-                                  pure (fpAcc', success && success1)
-
-                    Proj.Scanned Proj.Changed _ ms ->
-                      foldM f (fpAcc_, success_) ms
-                      where
-                        f (fpAcc, success) (m, _) =
-                         do let name = P.thing (P.mName m)
-                            checkRes <- checkModName 2 name
-                            let fpAcc' = Map.adjust (\fp -> fp { Proj.cacheDocstringResult = Just (crSuccess checkRes) }) (Proj.CacheInFile path) fpAcc
-                            pure (fpAcc', success && crSuccess checkRes)
+          (cache1, needCheck, success1) <-
+            foldM (updateStatus docstringResults) (cache0, [], True) (Map.assocs mp)
+          cacheId <- io (Proj.saveLoadCache (Proj.LoadCache cache1))
 
-              ) (cache0, True) (Map.assocs mp)
+          -- Revalidate modules, updating cache as you go
+          (_cacheId, cache, success) <- foldM doCheck (Just cacheId, cache1, success1) (reverse needCheck)
 
           let (passing, failing, missing) =
                 foldl
@@ -2406,8 +2371,60 @@
 
           rPutStrLn ("Passing: " ++ show passing ++ ", Failing: " ++ show failing ++ ", Missing: " ++ show missing)
 
-          _cacheId <- io (Proj.saveLoadCache (Proj.LoadCache cache))
           pure emptyCommandResult { crSuccess = success }
+
+  where
+  doCheck (cid, fpAcc, success) (path, m) =
+    do
+      let name = P.thing (P.mName m)
+      (newCid, checkRes) <- checkModName cid 2 name
+      let fpAcc' = Map.adjust (\fp -> fp { Proj.cacheDocstringResult = Just (crSuccess checkRes) }) (Proj.CacheInFile path) fpAcc
+      pure (newCid, fpAcc', success && crSuccess checkRes)
+
+  -- Check if some modules need to be revalidated.
+  updateStatus curCache (fpAcc_, needCheck_, success_) (k, v) =
+    case k of
+      M.InMem{} -> pure (fpAcc_, needCheck_, success_)
+
+      M.InFile path ->
+        case v of
+          Proj.Invalid e ->
+           do rPrint ("Failed to process module:" <+> (text path <> ":") $$
+                       indent 2 (ppInvalidStatus e))
+              pure (fpAcc_, needCheck_, False) -- report failure
+          Proj.Scanned Proj.Unchanged _ ms -> foldM f (fpAcc_, needCheck_, success_) ms
+            where
+              f (fpAcc, needCheck, success) (m, _) =
+               do let name = P.thing (P.mName m)
+                  case join (Map.lookup (Proj.CacheInFile path) curCache) of
+                    Just True  ->
+                     do rPrint ("Checking module" <+> hcat [pp name, ": PASS (cached)"])
+                        let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just True }) (Proj.CacheInFile path) fpAcc
+                        pure (fpAcc', needCheck, success) -- preserve success
+
+                    Just False ->
+                      case mode of
+                        Proj.UntestedMode Proj.RecheckFailed ->
+                          do
+                            let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Nothing }) (Proj.CacheInFile path) fpAcc
+                            pure (fpAcc', (path, m) : needCheck, success)
+                        _ ->
+                          do 
+                            rPrint ("Checking module" <+> hcat [pp name, ": FAIL (cached)"])
+                            let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Just False }) (Proj.CacheInFile path) fpAcc
+                            pure (fpAcc', needCheck, False) -- preserve fail
+                        
+                    Nothing -> pure (fpAcc', newNeedCheck, success)
+                      where
+                      fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Nothing }) (Proj.CacheInFile path) fpAcc
+                      newNeedCheck =
+                        case mode of
+                          Proj.ModifiedMode -> needCheck
+                          _                 -> (path, m) : needCheck
+                     
+          Proj.Scanned Proj.Changed _ ms -> pure (fpAcc', reverse pms ++ needCheck_, success_)
+            where pms = [ (path, m) | (m, _) <- ms ]
+                  fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = Nothing }) (Proj.CacheInFile path) fpAcc_              
 
 -- | Get the path to the SAW command.
 -- Search options, in order:
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
@@ -104,8 +104,10 @@
 import qualified Cryptol.ModuleSystem as M
 import qualified Cryptol.ModuleSystem.Env as M
 import qualified Cryptol.ModuleSystem.Name as M
+import qualified Cryptol.ModuleSystem.Names as M
 import qualified Cryptol.ModuleSystem.NamingEnv as M
 import Cryptol.Parser (ParseError,ppError)
+import Cryptol.Parser.Name (NameSource(..))
 import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
 import Cryptol.Parser.NoPat (Error)
 import Cryptol.Parser.Position (emptyRange, Range(from))
@@ -136,7 +138,7 @@
 import Data.IORef
     (IORef,newIORef,readIORef,atomicModifyIORef)
 import Data.List (intercalate, isPrefixOf, unfoldr, sortBy)
-import Data.Maybe (catMaybes)
+import Data.Maybe (catMaybes, isJust)
 import Data.Ord (comparing)
 import Data.Tuple (swap)
 import Data.Typeable (Typeable)
@@ -534,8 +536,6 @@
 getLoadedMod :: REPL (Maybe LoadedModule)
 getLoadedMod  = eLoadedMod `fmap` getRW
 
-
-
 -- | Set the path for the ':e' command.
 -- Note that this does not change the focused module (i.e., what ":r" reloads)
 setEditPath :: FilePath -> REPL ()
@@ -659,14 +659,19 @@
 getFocusedEnv  = M.focusedEnv <$> getModuleEnv
 
 -- | Get visible variable names.
--- This is used for command line completition.
+-- This is used for command line completion.
 getExprNames :: REPL [String]
 getExprNames =
-  do fNames <- M.mctxNames <$> getFocusedEnv
-     return (map (show . pp) (Map.keys (M.namespaceMap M.NSValue fNames)))
+  do 
+      fNames <- M.mctxNames <$> getFocusedEnv
+      let mnames = M.namespaceMap M.NSValue fNames
+      let userNamesMap = 
+                Map.filterWithKey (\_k v -> isJust (M.filterNames (\n -> UserName == M.nameSrc n) v)) mnames
+      return (map (show . pp) (Map.keys userNamesMap))
 
+
 -- | Get visible type signature names.
--- This is used for command line completition.
+-- This is used for command line completion.
 getTypeNames :: REPL [String]
 getTypeNames  =
   do fNames <- M.mctxNames <$> getFocusedEnv
@@ -788,7 +793,7 @@
 
 -- | Generate a fresh name using the given index. The name will reside within
 -- the "<interactive>" namespace.
-freshName :: I.Ident -> M.NameSource -> REPL M.Name
+freshName :: I.Ident -> NameSource -> REPL M.Name
 freshName i sys =
   M.liftSupply (M.mkDeclared I.NSValue mpath sys i Nothing emptyRange)
   where mpath = M.TopModule I.interactiveName
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
@@ -79,7 +79,7 @@
 module Cryptol.Transform.MonoValues (rewModule) where
 
 import Cryptol.ModuleSystem.Name
-        (SupplyT,liftSupply,Supply,mkDeclared,NameSource(..),ModPath(..))
+        (SupplyT,liftSupply,Supply,mkDeclared,ModPath(..), NameSource(..))
 import Cryptol.Parser.Position (emptyRange)
 import Cryptol.TypeCheck.AST hiding (splitTApp) -- XXX: just use this one
 import Cryptol.TypeCheck.TypeMap
diff --git a/src/Cryptol/TypeCheck/Default.hs b/src/Cryptol/TypeCheck/Default.hs
--- a/src/Cryptol/TypeCheck/Default.hs
+++ b/src/Cryptol/TypeCheck/Default.hs
@@ -22,10 +22,14 @@
 -- | We default constraints of the form @Literal t a@ and @FLiteral m n r a@.
 --
 --   For @Literal t a@ we examine the context of constraints on the type @a@
---   to decide how to default.  If @Logic a@ is required,
---   we cannot do any defaulting.  Otherwise, we default
---   to either @Integer@ or @Rational@.  In particular, if
---   we need to satisfy the @Field a@, constraint, we choose
+--   to decide how to default.
+-- 
+--   We do NOT default if:
+--     * `Logic t` and `a` in `fvs t`
+--     * `Integral t`, and `t /= a`, and `a` in `fvs t`
+--
+--   Otherwise, we default to either @Integer@ or @Rational@.
+--   In particular, if we need to satisfy the @Field a@, constraint, we choose
 --   @Rational@ and otherwise we choose @Integer@.
 --
 --   For @FLiteral t a@ we always default to @Rational@.
@@ -39,6 +43,20 @@
 
   isLiteralGoal a = isJust (Map.lookup a (literalGoals gSet)) ||
                     isJust (Map.lookup a (literalLessThanGoals gSet))
+
+  disableDefaultPred a p =
+    case pIsLogic p of
+      Just t -> a `Set.member` fvs t
+      Nothing ->
+        case pIsIntegral p of
+          Just t ->
+            case tIsVar t of
+              Just _  -> False 
+              Nothing -> a `Set.member` fvs t
+          Nothing -> False
+
+  disableDefault a = any (disableDefaultPred a) allProps
+
   tryDefVar a =
     -- If there is an `FLiteral` constraint we use that for defaulting.
     case Map.lookup a (flitDefaultCandidates gSet) of
@@ -46,10 +64,10 @@
 
       -- Otherwise we try to use a `Literal`
       Nothing
-        | isLiteralGoal a -> do
-           defT <- if has pLogic a then mzero
-                   else if has pField a && not (has pIntegral a)
-                          then pure tRational
+        | isLiteralGoal a && not (disableDefault a)  -> do
+           defT <- 
+                   if has pField a && not (has pIntegral a)
+                      then pure tRational
                    else if not (has pField a) then pure tInteger
                    else mzero
            let d    = tvInfo a
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
@@ -10,7 +10,7 @@
 import qualified Data.Set as Set
 import Control.DeepSeq(NFData)
 import GHC.Generics(Generic)
-import Data.List((\\),sortBy,partition)
+import Data.List((\\),sortBy,partition,intersperse)
 import Data.Function(on)
 
 import Cryptol.Utils.Ident(Ident,Namespace(..))
@@ -89,6 +89,7 @@
               | DefaultingWildType P.Kind
               | DefaultingTo !TVarInfo Type
               | NonExhaustivePropGuards Name
+              | DuplicateDeriving PC
                 deriving (Show, Generic, NFData)
 
 -- | Various errors that might happen during type checking/inference
@@ -117,6 +118,19 @@
                 --   More patterns provided for a bind than expected,
                 --   given its signature.
 
+              | ClassNotDerivable
+                -- ^ Deriving unsupported typeclass
+                  Name   -- ^ The thing that the user tried to derive
+                  String -- ^ Description of the type declaration
+                  [PC]   -- ^ The supported typeclasses for deriving on this
+                         --   sort of type declaration
+
+              | DerivingMissingSuperclasses
+                -- ^ Deriving instance for a class without deriving instances
+                --   for its superclasses
+                  PC   -- ^ The class listed in the deriving clause
+                  [PC] -- ^ Its superclasses not listed in the deriving clause
+
               | TypeMismatch TypeSource Path Type Type
                 -- ^ Expected type, inferred type
 
@@ -161,9 +175,9 @@
                 -- ^ Too many positional type arguments, in an explicit
                 -- type instantiation
 
-              | BadParameterKind TParam Kind
-                -- ^ Kind other than `*` or `#` given to parameter of
-                --   type synonym, newtype, function signature, etc.
+              | BadParameterKind TParam Kind [Kind]
+                -- ^ We expected one of the kinds in the list, but got
+                -- the given one instead.
 
               | CannotMixPositionalAndNamedTypeParams
 
@@ -245,6 +259,8 @@
     KindMismatch {}                                  -> 10
     TyVarWithParams {}                               -> 9
     TooManyParams{}                                  -> 9
+    ClassNotDerivable{}                              -> 8
+    DerivingMissingSuperclasses{}                    -> 8
     TypeMismatch {}                                  -> 8
     EnumTypeMismatch {}                              -> 7
     SchemaMismatch {}                                -> 7
@@ -301,6 +317,7 @@
       DefaultingWildType {} -> warn
       DefaultingTo d ty     -> DefaultingTo d $! (apSubst su ty)
       NonExhaustivePropGuards {} -> warn
+      DuplicateDeriving {}  -> warn
 
 instance FVS Warning where
   fvs warn =
@@ -309,6 +326,7 @@
       DefaultingWildType {} -> Set.empty
       DefaultingTo _ ty     -> fvs ty
       NonExhaustivePropGuards {} -> Set.empty
+      DuplicateDeriving {}  -> Set.empty
 
 instance TVars Error where
   apSubst su err =
@@ -322,6 +340,8 @@
       SchemaMismatch i t1 t2  ->
         SchemaMismatch i !$ (apSubst su t1) !$ (apSubst su t2)
       TooManyParams b t i j     -> TooManyParams b !$ (apSubst su t) .$ i .$ j
+      ClassNotDerivable {}      -> err
+      DerivingMissingSuperclasses {} -> err
       TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2)
       EnumTypeMismatch t        -> EnumTypeMismatch !$ apSubst su t
       InvalidConPat {}          -> err
@@ -375,6 +395,8 @@
       RecursiveTypeDecls {}     -> Set.empty
       SchemaMismatch _ t1 t2    -> fvs (t1,t2)
       TooManyParams _ t _ _     -> fvs t
+      ClassNotDerivable {}      -> Set.empty
+      DerivingMissingSuperclasses {} -> Set.empty
       TypeMismatch _ _ t1 t2    -> fvs (t1,t2)
       EnumTypeMismatch t        -> fvs t
       InvalidConPat {}          -> Set.empty
@@ -393,7 +415,7 @@
       UndefinedTypeParameter {}             -> Set.empty
       RepeatedTypeParameter {}              -> Set.empty
       AmbiguousSize _ t -> fvs t
-      BadParameterKind tp _ -> Set.singleton (TVBound tp)
+      BadParameterKind tp _ _ -> Set.singleton (TVBound tp)
 
       BareTypeApp -> Set.empty
 
@@ -440,6 +462,9 @@
         text "Could not prove that the constraint guards used in defining" <+>
         pp n <+> text "were exhaustive."
 
+      DuplicateDeriving pc ->
+        "Duplicate" <+> pp pc <+> "in deriving clause"
+
 instance PP (WithNames Error) where
   ppPrec _ (WithNames err names) =
     case err of
@@ -506,6 +531,16 @@
             , "Actual number of parameters:" <+> int i
             , "When defining" <+> quotes ((pp n <> ":") <+> ppWithNames names t) ]
 
+      ClassNotDerivable badCls declDesc allowed ->
+        "Cannot derive" <+> backticks (pp badCls) $$
+        nested ("Derivable constraints for" <+> text declDesc <+> "declarations are:")
+          (commaSepFill (map pp allowed))
+
+      DerivingMissingSuperclasses pc supers ->
+        "Missing superclass(es) for" <+> pp pc $$
+        "To derive this constraint, you must also derive:" <+>
+          commaSepFill (map pp supers)
+
       TypeMismatch src pa t1 t2 ->
         addTVarsDescsAfter names err $
         nested "Type mismatch:" $
@@ -600,10 +635,11 @@
                    ++ [ "When checking" <+> pp src ]
                )
 
-      BadParameterKind tp k ->
+      BadParameterKind tp k ks ->
         addTVarsDescsAfter names err $
         vcat [ "Illegal kind assigned to type variable:" <+> ppWithNames names tp
-             , "Unexpected:" <+> pp k
+             , "Expected:" <+> hsep (intersperse "or" (map pp ks))
+             , "Actual:" <+> pp k
              ]
 
       TooManyPositionalTypeParams ->
diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs
--- a/src/Cryptol/TypeCheck/InferTypes.hs
+++ b/src/Cryptol/TypeCheck/InferTypes.hs
@@ -231,8 +231,24 @@
   | CtPropGuardsExhaustive Name -- ^ Checking that a use of prop guards is exhastive
   | CtFFI Name            -- ^ Constraints on a foreign declaration required
                           --   by the FFI (e.g. sequences must be finite)
+  | CtDeriving            -- ^ Required conditions for deriving
+      Name                     -- ^ The type that the deriving clause is
+                               --   attached to
+      PC                       -- ^ The class we are deriving
+      DerivingConstraintSource -- ^ Which part of the type declaration caused
+                               --   this constraint
     deriving (Show, Generic, NFData)
 
+-- | Where a condition for deriving arises from
+data DerivingConstraintSource
+  = NewtypeUnderlyingRecord -- ^ From the underlying record, when deriving for a
+                            --   newtype
+  | EnumCtorField           -- ^ From a constructor field of an enum
+      Name -- ^ Name of the constructor
+      Int  -- ^ Index of the constructor field, starting from 0
+      Type -- ^ Type of the constructor field
+  deriving (Show, Generic, NFData)
+
 selSrc :: Selector -> TypeSource
 selSrc l = case l of
              RecordSel la _ -> TypeOfRecordField la
@@ -249,7 +265,7 @@
       CtComprehension -> src
       CtSplitPat      -> src
       CtTypeSig       -> src
-      CtInst e        -> CtInst (apSubst su e)
+      CtInst e        -> CtInst $! apSubst su e
       CtSelector      -> src
       CtExactType     -> src
       CtEnumeration   -> src
@@ -260,8 +276,15 @@
       CtModuleInstance _ -> src
       CtPropGuardsExhaustive _ -> src
       CtFFI _          -> src
+      CtDeriving t p w -> CtDeriving t p $! apSubst su w
 
+instance TVars DerivingConstraintSource where
+  apSubst su src =
+    case src of
+      NewtypeUnderlyingRecord -> src
+      EnumCtorField c i t     -> EnumCtorField c i $! apSubst su t
 
+
 instance FVS Goal where
   fvs g = fvs (goal g)
 
@@ -371,6 +394,17 @@
       CtModuleInstance r -> "module instantiation at" <+> pp r
       CtPropGuardsExhaustive n -> "exhaustion check for prop guards used in defining" <+> pp n
       CtFFI f         -> "declaration of foreign function" <+> pp f
+      CtDeriving t pc which -> pp which $$
+                               "when deriving instance" <+> parens (pp pc <+> pp t)
+
+instance PP DerivingConstraintSource where
+  ppPrec _ src =
+    case src of
+      NewtypeUnderlyingRecord -> "the underlying record of the newtype"
+      EnumCtorField ctor i t ->
+        -- Count starting from 1 when displaying to user
+        "field" <+> int (i + 1) <+> "of constructor" <+> backticks (pp ctor) <+>
+        parens ("type" <+> backticks (pp t))
 
 ppUse :: Expr -> Doc
 ppUse expr =
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
@@ -25,20 +25,27 @@
 
 import qualified Cryptol.Parser.AST as P
 import           Cryptol.Parser.Position
+import           Cryptol.ModuleSystem.Name(nameLoc)
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Error
-import           Cryptol.TypeCheck.Subst(listSubst,apSubst)
+import           Cryptol.TypeCheck.Subst(listSubst,apSubst,isEmptySubst)
 import           Cryptol.TypeCheck.Monad hiding (withTParams)
 import           Cryptol.TypeCheck.SimpType(tRebuild)
 import           Cryptol.TypeCheck.SimpleSolver(simplify)
-import           Cryptol.TypeCheck.Solve (simplifyAllConstraints)
+import           Cryptol.TypeCheck.Solve ( buildSolverCtxt
+                                         , quickSolver
+                                         , simplifyAllConstraints
+                                         )
 import           Cryptol.Utils.Panic (panic)
 import           Cryptol.Utils.PP(pp,commaSep)
 import           Cryptol.Utils.RecordMap
 
+import           Data.Map (Map)
 import qualified Data.Map as Map
+import qualified Data.Set as Set
+import           Data.Foldable(foldlM)
 import           Data.List(sortBy,groupBy)
-import           Data.Maybe(fromMaybe)
+import           Data.Maybe(fromMaybe,isJust)
 import           Data.Function(on)
 import           Data.Text (Text)
 import           Control.Monad(unless,mplus,forM,when)
@@ -91,15 +98,35 @@
 
 
 
--- | Check a module parameter declarations.  Nothing much to check,
--- we just translate from one syntax to another.
+-- | Check a module parameter declaration.
+-- We check that it has kind either * or #.
 checkParameterType :: P.ParameterType Name -> InferM ModTParam
 checkParameterType a =
-  do let mbDoc = P.ptDoc a
-         k = cvtK (P.ptKind a)
-         n = thing (P.ptName a)
-     return ModTParam { mtpKind = k, mtpName = n, mtpDoc = thing <$> mbDoc }
-
+  do
+    let
+      mbDoc = P.ptDoc a
+      k  = cvtK (P.ptKind a)
+      n  = thing (P.ptName a)
+      mp = ModTParam { mtpKind = k, mtpName = n, mtpDoc = thing <$> mbDoc }
+    case k of
+      KNum -> pure mp
+      KType -> pure mp
+      _ ->
+        do
+          let mp' = mp { mtpKind = someKind k }
+          inRange (nameLoc n)
+            $ recordError (BadParameterKind (mtpParam mp') k [KNum,KType])
+          pure mp'
+  where
+  -- When we find a malformed kind, we report an error, and correct the kind
+  -- according to this function, as the rest of the code expects one of
+  -- these kinds.
+  someKind e =
+    case e of
+      _ :-> x -> someKind x
+      KNum  -> KNum
+      KType -> KType
+      KProp -> KType
 
 -- | Check a type-synonym declaration.
 checkTySyn :: P.TySyn Name -> Maybe Text -> InferM TySyn
@@ -135,8 +162,8 @@
 
 -- | Check a newtype declaration.
 checkNewtype :: P.Newtype Name -> Maybe Text -> InferM NominalType
-checkNewtype (P.Newtype x as con fs) mbD =
-  do ((as1,fs1),gs) <- collectGoals $
+checkNewtype (P.Newtype x as con fs derivs) mbDoc =
+  do ((as1,fs1),bodyGs) <- collectGoals $
        inRange (srcRange x) $
        do r <- withTParams NoWildCards nominalParam as $
                flip traverseRecordMap fs $ \_n (rng,f) ->
@@ -144,17 +171,32 @@
           simplifyAllConstraints
           return r
 
+     let name = thing x
+         constraints = map goal bodyGs
+     derivConds <-
+       checkDeriving name newtypeDerivable derivs constraints
+         [(TRec fs1, NewtypeUnderlyingRecord)]
+
      return NominalType
                     { ntName   = thing x
                     , ntKind   = KType
                     , ntParams = as1
-                    , ntConstraints = map goal gs
+                    , ntConstraints = constraints
                     , ntDef = Struct
                                 StructCon { ntConName = con, ntFields = fs1 }
+                    , ntDeriving = derivConds
                     , ntFixity = Nothing
-                    , ntDoc = mbD
+                    , ntDoc = mbDoc
                     }
 
+-- | A description of newtype declarations, and the supported classes for
+-- deriving on newtypes.
+newtypeDerivable :: (String, [PC])
+newtypeDerivable =
+  ( "newtype"
+  , [PEq, PCmp, PSignedCmp, PZero, PLogic, PRing]
+  )
+
 checkEnum :: P.EnumDecl Name -> Maybe Text -> InferM NominalType
 checkEnum ed mbD =
   do let x = P.eName ed
@@ -175,16 +217,121 @@
                           }
           simplifyAllConstraints
           pure r
+
+     let name = thing x
+         constraints = map goal gs
+     derivConds <-
+       checkDeriving name enumDerivable (P.eDeriving ed) constraints $
+         concatMap
+           (\con -> zipWith (\t i -> (t, EnumCtorField (ecName con) i t))
+                            (ecFields con)
+                            [0..])
+           cons1
+
      pure NominalType
                   { ntName = thing x
                   , ntParams = as1
                   , ntKind = KType
-                  , ntConstraints = map goal gs
+                  , ntConstraints = constraints
                   , ntDef = Enum cons1
+                  , ntDeriving = derivConds
                   , ntFixity = Nothing
                   , ntDoc = mbD
                   }
 
+-- | A description of enum declarations, and the supported classes for deriving
+-- on enums.
+enumDerivable :: (String, [PC])
+enumDerivable =
+  ( "enum"
+  , [PEq, PCmp, PSignedCmp]
+  )
+
+-- | Check a deriving clause, returning the derived classes and any conditions
+-- that must be satisfied for the instances to hold.
+checkDeriving ::
+     Name
+     -- ^ the type being declared
+  -> (String, [PC])
+     -- ^ description of the type being declared, and the allowed typeclasses
+     -- for deriving on this sort of declaration
+  -> [Located Name]
+     -- ^ list of names in the @deriving@ clause
+  -> [Prop]
+     -- ^ constraints generated from the type declaration's body
+  -> [(Type, DerivingConstraintSource)]
+     -- ^ field types within the type declaration, and where they come from
+  -> InferM (Map PC [Prop])
+     -- ^ map from derived typeclasses to their conditions
+checkDeriving declName (declDesc, allowed) derivs constraints fieldTypes = do
+  -- Check that the names in the deriving clause are allowed and contain no
+  -- duplicates.
+  let addDerivRange derivRangeMap deriv = do
+        let derivName = thing deriv
+            derivRange = srcRange deriv
+        case builtInType derivName of
+          Just (PC pc)
+            | pc `elem` allowed -> do
+              let (existing, derivRangeMap') =
+                    Map.insertLookupWithKey (\_ _ old -> old)
+                                            pc
+                                            derivRange
+                                            derivRangeMap
+              when (isJust existing) $
+                inRange derivRange $
+                  recordWarning $ DuplicateDeriving pc
+              pure derivRangeMap'
+          _ -> do
+            recordErrorLoc (Just derivRange) $
+              ClassNotDerivable derivName declDesc allowed
+            pure derivRangeMap
+  derivRangeMap <- foldlM addDerivRange mempty derivs
+  -- We can use the functor constraints and the constraints generated from the
+  -- body of the type declaration as assumptions for the solver.
+  paramConstraints <- getParamConstraints
+  let ctxt = buildSolverCtxt (constraints ++ map thing paramConstraints)
+  -- For each derived class, generate its conditions.
+  let generateConds pc derivRange = do
+        -- Ensure superclasses are explicitly derived.
+        let missingSuperclasses =
+              Set.difference (typeSuperclassSet pc) (Map.keysSet derivRangeMap)
+        unless (null missingSuperclasses) $
+          recordErrorLoc (Just derivRange) $
+            DerivingMissingSuperclasses pc (Set.toList missingSuperclasses)
+        -- All fields in the type declaration must be instances of each class.
+        let goals =
+              map (\(ty, which) ->
+                    Goal { goal = TCon (PC pc) [ty]
+                         , goalSource = CtDeriving declName pc which
+                         , goalRange = derivRange
+                         })
+                  fieldTypes
+        case quickSolver ctxt goals of
+          Right (su, conds)
+            -- Since we are not doing type inference, su should be empty.
+            | isEmptySubst su ->
+              -- conds contains the goals that the solver was unable to solve,
+              -- but unable to rule out either (e.g. goals involving a type
+              -- parameter, which can only be solved when this nominal type is
+              -- actually used). These are the conditions that we want to save
+              -- in the 'NominalType', so they can be checked at the use site of
+              -- the class methods.
+              pure $ Just $ map goal conds
+            | otherwise ->
+              panic "checkDeriving"
+                [ "Solver substitution not empty"
+                , "ctxt: " ++ show ctxt
+                , "goals: " ++ show goals
+                , "su: " ++ show su
+                , "conds: " ++ show conds
+                ]
+          Left err -> do
+            -- If there were unsolvable (impossible) goals, that means some
+            -- fields were not instances of this class. Report the error here.
+            recordErrorLoc (Just derivRange) err
+            pure Nothing
+  Map.traverseMaybeWithKey generateConds derivRangeMap
+
 checkPrimType :: P.PrimType Name -> Maybe Text -> InferM NominalType
 checkPrimType p mbD =
   do let (as,cs) = P.primTCts p
@@ -205,6 +352,7 @@
             , ntConstraints = cs'
             , ntDoc = mbD
             , ntDef = Abstract
+            , ntDeriving = mempty
             }
   where
   splitK k =
diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs
--- a/src/Cryptol/TypeCheck/ModuleInstance.hs
+++ b/src/Cryptol/TypeCheck/ModuleInstance.hs
@@ -111,6 +111,7 @@
             , ntKind        = ntKind nt
             , ntConstraints = moduleInstance (ntConstraints nt)
             , ntDef         = moduleInstance (ntDef nt)
+            , ntDeriving    = moduleInstance <$> ntDeriving nt
             , ntFixity      = ntFixity nt
             , ntDoc         = ntDoc nt
             }
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
@@ -39,7 +39,7 @@
 
 import           Cryptol.ModuleSystem.Name
                     (FreshM(..),Supply,mkLocal,asLocal
-                    , nameInfo, NameInfo(..),NameSource(..), nameTopModule)
+                    , nameInfo, NameInfo(..),NameSource(..),nameTopModule)
 import           Cryptol.ModuleSystem.NamingEnv.Types
 import qualified Cryptol.ModuleSystem.Interface as If
 import           Cryptol.Parser.Position
@@ -633,13 +633,13 @@
         KNum  -> return ()
         KType -> return ()
         KProp -> return ()
-        _ -> recordError (BadParameterKind tp k)
+        _ -> recordError (BadParameterKind tp k [KNum, KType, KProp])
 
     starOrHash =
       case k of
         KNum  -> return ()
         KType -> return ()
-        _ -> recordError (BadParameterKind tp k)
+        _ -> recordError (BadParameterKind tp k [KNum,KType])
 
 -- | Generate a new free type variable.
 newTParam :: P.TParam Name -> TPFlavor -> Kind -> InferM TParam
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
@@ -7,7 +7,8 @@
 import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
 import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq, cryIsPrime)
 import Cryptol.TypeCheck.Solver.Class
-  ( solveZeroInst, solveLogicInst, solveRingInst
+  ( solveDerivedInst
+  , solveZeroInst, solveLogicInst, solveRingInst
   , solveIntegralInst, solveFieldInst, solveRoundInst
   , solveEqInst, solveCmpInst, solveSignedCmpInst
   , solveLiteralInst
@@ -46,6 +47,9 @@
   case tNoUser prop of
     TCon (PC PTrue)  []        -> SolvedIf []
     TCon (PC PAnd)   [l,r]     -> SolvedIf [l,r]
+
+    TCon (PC pc) [ty]
+      | TNominal nt targs <- tNoUser ty -> solveDerivedInst pc nt targs
 
     TCon (PC PZero)  [ty]      -> solveZeroInst ty
     TCon (PC PLogic) [ty]      -> solveLogicInst ty
diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs
--- a/src/Cryptol/TypeCheck/Solve.hs
+++ b/src/Cryptol/TypeCheck/Solve.hs
@@ -14,6 +14,8 @@
   , proveModuleTopLevel
   , defaultAndSimplify
   , defaultReplExpr
+  , quickSolver
+  , buildSolverCtxt
   ) where
 
 import           Cryptol.Parser.Position(thing,emptyRange)
diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs
--- a/src/Cryptol/TypeCheck/Solver/Class.hs
+++ b/src/Cryptol/TypeCheck/Solver/Class.hs
@@ -11,7 +11,11 @@
 
 {-# LANGUAGE PatternGuards #-}
 module Cryptol.TypeCheck.Solver.Class
-  ( solveZeroInst
+  ( solveDerivedInst
+    -- * Built-in instances
+    --
+    -- $builtInInstances
+  , solveZeroInst
   , solveLogicInst
   , solveRingInst
   , solveFieldInst
@@ -26,11 +30,13 @@
   , solveValidFloat
   ) where
 
+import qualified Data.Map as Map
 import qualified LibBF as FP
 
 import Cryptol.TypeCheck.Type hiding (tSub)
 import Cryptol.TypeCheck.SimpType (tAdd,tSub,tWidth,tMax)
 import Cryptol.TypeCheck.Solver.Types
+import Cryptol.TypeCheck.Subst.Type (listParamSubst, apSubstNoSimp)
 import Cryptol.Utils.RecordMap
 
 {- | This places constraints on the floating point numbers that
@@ -65,6 +71,25 @@
 
 
 
+-- | Solve a constraint on a nominal type by looking up its derived instance.
+solveDerivedInst :: PC          -- ^ the typeclass (of kind @* -> Prop@)
+                 -> NominalType -- ^ the type constructor
+                 -> [Type]      -- ^ type arguments to the 'NominalType'
+                 -> Solved
+solveDerivedInst pc nt targs =
+  case Map.lookup pc (ntDeriving nt) of
+    Just conds ->
+      -- The conditions saved in the type may refer to the type parameters, so
+      -- we need to instantiate them with the type arguments.
+      let subst = listParamSubst $ zip (ntParams nt) targs
+      in  SolvedIf $ map (apSubstNoSimp subst) conds
+    Nothing -> Unsolvable
+
+-- $builtInInstances
+-- The functions below only solve for built-in instances. To solve for derived
+-- instances, check first if the type is 'TNominal' and use 'solveDerivedInst'
+-- in that case.
+
 -- | Solve a Zero constraint by instance, if possible.
 solveZeroInst :: Type -> Solved
 solveZeroInst ty = case tNoUser ty of
@@ -101,9 +126,6 @@
   -- (Zero a, Zero b) => Zero { x1 : a, x2 : b }
   TRec fs -> SolvedIf [ pZero ety | ety <- recordElements fs ]
 
-  -- Zero <nominal> -> fails
-  TNominal {} -> Unsolvable
-
   _ -> Unsolved
 
 -- | Solve a Logic constraint by instance, if possible.
@@ -140,9 +162,6 @@
   -- (Logic a, Logic b) => Logic { x1 : a, x2 : b }
   TRec fs -> SolvedIf [ pLogic ety | ety <- recordElements fs ]
 
-  -- Logic <nominal> -> fails
-  TNominal {} -> Unsolvable
-
   _ -> Unsolved
 
 
@@ -180,9 +199,6 @@
   -- (Ring a, Ring b) => Ring { x1 : a, x2 : b }
   TRec fs -> SolvedIf [ pRing ety | ety <- recordElements fs ]
 
-  -- Ring <nominal> -> fails
-  TNominal {} -> Unsolvable
-
   _ -> Unsolved
 
 
@@ -350,9 +366,6 @@
   -- (Eq a, Eq b) => Eq { x:a, y:b }
   TRec fs -> SolvedIf [ pEq e | e <- recordElements fs ]
 
-  -- Eq <nominal> -> fails
-  TNominal {} -> Unsolvable
-
   _ -> Unsolved
 
 
@@ -390,9 +403,6 @@
   -- (Cmp a, Cmp b) => Cmp { x:a, y:b }
   TRec fs -> SolvedIf [ pCmp e | e <- recordElements fs ]
 
-  -- Cmp <nominal> -> fails
-  TNominal{} -> Unsolvable
-
   _ -> Unsolved
 
 
@@ -444,9 +454,6 @@
 
   -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b }
   TRec fs -> SolvedIf [ pSignedCmp e | e <- recordElements fs ]
-
-  -- SignedCmp <nominal> -> fails
-  TNominal{} -> Unsolvable
 
   _ -> Unsolved
 
diff --git a/src/Cryptol/TypeCheck/Solver/Improve.hs b/src/Cryptol/TypeCheck/Solver/Improve.hs
--- a/src/Cryptol/TypeCheck/Solver/Improve.hs
+++ b/src/Cryptol/TypeCheck/Solver/Improve.hs
@@ -20,7 +20,7 @@
 
 -- | Improvements from a bunch of propositions.
 -- Invariant:
--- the substitions should be already applied to the new sub-goals, if any.
+-- the substitutions should be already applied to the new sub-goals, if any.
 improveProps :: Bool -> Ctxt -> [Prop] -> Match (Subst,[Prop])
 improveProps impSkol ctxt ps0 = loop emptySubst ps0
   where
@@ -40,13 +40,25 @@
 
 -- | Improvements from a proposition.
 -- Invariant:
--- the substitions should be already applied to the new sub-goals, if any.
+-- the substitutions should be already applied to the new sub-goals, if any.
 improveProp :: Bool -> Ctxt -> Prop -> Match (Subst,[Prop])
 improveProp impSkol ctxt prop =
   improveEq impSkol ctxt prop <|>
-  improveLit impSkol prop
+  improveLit impSkol prop <|>
+  improveIntegral impSkol prop
   -- XXX: others
 
+-- Whenever we have `Integral [m]a`, we can learn that `a = Bit`
+improveIntegral :: Bool -> Prop -> Match (Subst,[Prop])
+improveIntegral impSkol prop =
+  do
+    t     <- aIntegral prop
+    (_,b) <- aSeq t
+    a     <- aTVar b
+    unless impSkol $ guard (isFreeTV a)
+    let su = uncheckedSingleSubst a tBit
+    return (su, [])
+
 -- Whenever we have `Literal n [m]a`,
 -- we can learn that `a = Bit`
 improveLit :: Bool -> Prop -> Match (Subst, [Prop])
@@ -61,7 +73,7 @@
 
 -- | Improvements from equality constraints.
 -- Invariant:
--- the substitions should be already applied to the new sub-goals, if any.
+-- the substitutions should be already applied to the new sub-goals, if any.
 improveEq :: Bool -> Ctxt -> Prop -> Match (Subst,[Prop])
 improveEq impSkol fins prop =
   do (lhs,rhs) <- (|=|) prop
diff --git a/src/Cryptol/TypeCheck/Solver/Types.hs b/src/Cryptol/TypeCheck/Solver/Types.hs
--- a/src/Cryptol/TypeCheck/Solver/Types.hs
+++ b/src/Cryptol/TypeCheck/Solver/Types.hs
@@ -13,7 +13,7 @@
   SolverCtxt
   { intervals :: Map TVar Interval
   , saturatedAsmps :: Set Prop
-  }
+  } deriving Show
 
 instance Semigroup Ctxt where
   SolverCtxt is1 as1 <> SolverCtxt is2 as2 = SolverCtxt (is1 <> is2) (as1 <> as2)
diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs
--- a/src/Cryptol/TypeCheck/Subst.hs
+++ b/src/Cryptol/TypeCheck/Subst.hs
@@ -9,8 +9,6 @@
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE Safe #-}
 module Cryptol.TypeCheck.Subst
   ( Subst
@@ -39,109 +37,12 @@
 import           Data.Either (partitionEithers)
 import qualified Data.Map.Strict as Map
 import qualified Data.IntMap as IntMap
-import           Data.Set (Set)
-import qualified Data.Set as Set
 
 import Cryptol.TypeCheck.AST
-import Cryptol.TypeCheck.PP
+import Cryptol.TypeCheck.Subst.Type
 import Cryptol.TypeCheck.TypeMap
-import qualified Cryptol.TypeCheck.SimpType as Simp
 import qualified Cryptol.TypeCheck.SimpleSolver as Simp
-import Cryptol.Utils.Panic(panic)
-import Cryptol.Utils.Misc (anyJust, anyJust2)
 
--- | A 'Subst' value represents a substitution that maps each 'TVar'
--- to a 'Type'.
---
--- Invariant 1: If there is a mapping from @TVFree _ _ tps _@ to a
--- type @t@, then @t@ must not mention (directly or indirectly) any
--- type parameter that is not in @tps@. In particular, if @t@ contains
--- a variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
--- @tps@. This ensures that applying the substitution will not permit
--- any type parameter to escape from its scope.
---
--- Invariant 2: The substitution must be idempotent, in that applying
--- a substitution to any 'Type' in the map should leave that 'Type'
--- unchanged. In other words, 'Type' values in the range of a 'Subst'
--- should not mention any 'TVar' in the domain of the 'Subst'. In
--- particular, this implies that a substitution must not contain any
--- recursive variable mappings.
---
--- Invariant 3: The substitution must be kind correct: Each 'TVar' in
--- the substitution must map to a 'Type' of the same kind.
-
-data Subst = S { suFreeMap :: !(IntMap.IntMap (TVar, Type))
-               , suBoundMap :: !(IntMap.IntMap (TVar, Type))
-               , suDefaulting :: !Bool
-               }
-                  deriving Show
-
-emptySubst :: Subst
-emptySubst =
-  S { suFreeMap = IntMap.empty
-    , suBoundMap = IntMap.empty
-    , suDefaulting = False
-    }
-
-mergeDistinctSubst :: [Subst] -> Subst
-mergeDistinctSubst sus =
-  case sus of
-    [] -> emptySubst
-    _  -> foldr1 merge sus
-
-  where
-  merge s1 s2 = S { suFreeMap     = jn suFreeMap s1 s2
-                  , suBoundMap    = jn suBoundMap s1 s2
-                  , suDefaulting  = if suDefaulting s1 || suDefaulting s2
-                                      then err
-                                      else False
-                  }
-
-  err       = panic "mergeDistinctSubst" [ "Not distinct" ]
-  bad _ _   = err
-  jn f x y  = IntMap.unionWith bad (f x) (f y)
-
-
-
-
-
-
--- | Reasons to reject a single-variable substitution.
-data SubstError
-  = SubstRecursive
-  -- ^ 'TVar' maps to a type containing the same variable.
-  | SubstEscaped [TParam]
-  -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.
-  | SubstKindMismatch Kind Kind
-  -- ^ 'TVar' maps to a type with a different kind.
-
-singleSubst :: TVar -> Type -> Either SubstError Subst
-singleSubst x t
-  | kindOf x /= kindOf t   = Left (SubstKindMismatch (kindOf x) (kindOf t))
-  | x `Set.member` fvs t   = Left SubstRecursive
-  | not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped))
-  | otherwise              = Right (uncheckedSingleSubst x t)
-  where
-    escaped =
-      case x of
-        TVBound _ -> Set.empty
-        TVFree _ _ scope _ -> freeParams t `Set.difference` scope
-
-uncheckedSingleSubst :: TVar -> Type -> Subst
-uncheckedSingleSubst v@(TVFree i _ _tps _) t =
-  S { suFreeMap = IntMap.singleton i (v, t)
-    , suBoundMap = IntMap.empty
-    , suDefaulting = False
-    }
-uncheckedSingleSubst v@(TVBound tp) t =
-  S { suFreeMap = IntMap.empty
-    , suBoundMap = IntMap.singleton (tpUnique tp) (v, t)
-    , suDefaulting = False
-    }
-
-singleTParamSubst :: TParam -> Type -> Subst
-singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t
-
 (@@) :: Subst -> Subst -> Subst
 s2 @@ s1
   | isEmptySubst s2 =
@@ -156,72 +57,8 @@
     , suDefaulting = suDefaulting s1 || suDefaulting s2
     }
 
--- | A defaulting substitution maps all otherwise-unmapped free
--- variables to a kind-appropriate default type (@Bit@ for value types
--- and @0@ for numeric types).
-defaultingSubst :: Subst -> Subst
-defaultingSubst s = s { suDefaulting = True }
 
--- | Makes a substitution out of a list.
--- WARNING: We do not validate the list in any way, so the caller should
--- ensure that we end up with a valid (e.g., idempotent) substitution.
-listSubst :: [(TVar, Type)] -> Subst
-listSubst xs
-  | null xs   = emptySubst
-  | otherwise = S { suFreeMap = IntMap.fromList frees
-                  , suBoundMap = IntMap.fromList bounds
-                  , suDefaulting = False }
-  where
-    (frees, bounds) = partitionEithers (map classify xs)
-    classify x =
-      case fst x of
-        TVFree i _ _ _ -> Left (i, x)
-        TVBound tp -> Right (tpUnique tp, x)
 
--- | Makes a substitution out of a list.
--- WARNING: We do not validate the list in any way, so the caller should
--- ensure that we end up with a valid (e.g., idempotent) substitution.
-listParamSubst :: [(TParam, Type)] -> Subst
-listParamSubst xs
-  | null xs   = emptySubst
-  | otherwise = S { suFreeMap = IntMap.empty
-                  , suBoundMap = IntMap.fromList bounds
-                  , suDefaulting = False }
-  where
-    bounds = [ (tpUnique tp, (TVBound tp, t)) | (tp, t) <- xs ]
-
-isEmptySubst :: Subst -> Bool
-isEmptySubst su = IntMap.null (suFreeMap su) && IntMap.null (suBoundMap su)
-
--- Returns the empty set if this is a defaulting substitution
-substBinds :: Subst -> Set TVar
-substBinds su
-  | suDefaulting su = Set.empty
-  | otherwise       = Set.fromList (map fst (assocsSubst su))
-
-substToList :: Subst -> [(TVar, Type)]
-substToList s
-  | suDefaulting s = panic "substToList" ["Defaulting substitution."]
-  | otherwise = assocsSubst s
-
-assocsSubst :: Subst -> [(TVar, Type)]
-assocsSubst s = frees ++ bounds
-  where
-    frees = IntMap.elems (suFreeMap s)
-    bounds = IntMap.elems (suBoundMap s)
-
-instance PP (WithNames Subst) where
-  ppPrec _ (WithNames s mp)
-    | null els  = text "(empty substitution)"
-    | otherwise = text "Substitution:" $$ nest 2 (vcat (map pp1 els))
-    where pp1 (x,t) = ppWithNames mp x <+> text "=" <+> ppWithNames mp t
-          els       = assocsSubst s
-
-instance PP Subst where
-  ppPrec n = ppWithNamesPrec IntMap.empty n
-
-
-
 infixl 0 !$
 infixl 0 .$
 
@@ -247,69 +84,12 @@
   where f' x = Done $! f x
 
 -- | Apply a substitution.  Returns `Nothing` if nothing changed.
+-- Performs simplification on the result.
 apSubstMaybe :: Subst -> Type -> Maybe Type
-apSubstMaybe su ty =
-  case ty of
-    TCon t ts ->
-      do ss <- anyJust (apSubstMaybe su) ts
-         case t of
-           TF _ -> Just $! Simp.tCon t ss
-           PC _ -> Just $! Simp.simplify mempty (TCon t ss)
-           _    -> Just (TCon t ss)
-
-    TUser f ts t ->
-      do (ts1, t1) <- anyJust2 (anyJust (apSubstMaybe su)) (apSubstMaybe su) (ts, t)
-         Just (TUser f ts1 t1)
-
-    TRec fs -> TRec `fmap` (anyJust (apSubstMaybe su) fs)
-
-    {- We apply the substitution to nominal types as well, because it might
-    contain module parameters, which need to be substituted when
-    instantiating a functor. -}
-    TNominal nt ts ->
-      uncurry TNominal <$> anyJust2 (applySubstToNominalType su)
-                                    (anyJust (apSubstMaybe su))
-                                    (nt,ts)
-
-    TVar x -> applySubstToVar su x
-
-lookupSubst :: TVar -> Subst -> Maybe Type
-lookupSubst x su =
-  fmap snd $
-  case x of
-    TVFree i _ _ _ -> IntMap.lookup i (suFreeMap su)
-    TVBound tp -> IntMap.lookup (tpUnique tp) (suBoundMap su)
+apSubstMaybe = apSubstMaybe' (Simp.simplify mempty)
 
 applySubstToVar :: Subst -> TVar -> Maybe Type
-applySubstToVar su x =
-  case lookupSubst x su of
-    -- For a defaulting substitution, we must recurse in order to
-    -- replace unmapped free vars with default types.
-    Just t
-      | suDefaulting su -> Just $! apSubst su t
-      | otherwise       -> Just t
-    Nothing
-      | suDefaulting su -> Just $! defaultFreeVar x
-      | otherwise       -> Nothing
-
-
-applySubstToNominalType :: Subst -> NominalType -> Maybe NominalType
-applySubstToNominalType su nt =
- do (cs,def)  <- anyJust2 (anyJust (apSubstMaybe su)) apSubstDef
-                          (ntConstraints nt, ntDef nt)
-    pure nt { ntConstraints = cs, ntDef = def }
-  where
-  apSubstDef d =
-    case d of
-      Struct c ->
-        do fs <- anyJust (apSubstMaybe su) (ntFields c)
-           pure (Struct c { ntFields = fs })
-      Enum cs -> Enum <$> anyJust apSubstCon cs
-      Abstract -> pure Abstract
-
-  apSubstCon c =
-    do fs <- anyJust (apSubstMaybe su) (ecFields c)
-       pure c { ecFields = fs }
+applySubstToVar = applySubstToVar' apSubstMaybe
 
 
 
@@ -333,18 +113,6 @@
 
 instance TVars Type where
   apSubst su ty = fromMaybe ty (apSubstMaybe su ty)
-
--- | Pick types for unconstrained unification variables.
-defaultFreeVar :: TVar -> Type
-defaultFreeVar x@(TVBound {}) = TVar x
-defaultFreeVar (TVFree _ k _ d) =
-  case k of
-    KType -> tBit
-    KNum  -> tNum (0 :: Int)
-    _     -> panic "Cryptol.TypeCheck.Subst.defaultFreeVar"
-                  [ "Free variable of unexpected kind."
-                  , "Source: " ++ show d
-                  , "Kind: " ++ show (pp k) ]
 
 instance (Traversable m, TVars a) => TVars (List m a) where
   apSubst su = fmap' (apSubst su)
diff --git a/src/Cryptol/TypeCheck/Subst/Type.hs b/src/Cryptol/TypeCheck/Subst/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Cryptol/TypeCheck/Subst/Type.hs
@@ -0,0 +1,293 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+-- | Most of this module is re-exported by "Cryptol.TypeCheck.Subst", so you
+-- probably want to import that instead of this.
+--
+-- The exception being, if you want to substitute types without performing
+-- simplification afterwards, then you should use 'apSubstNoSimp' from this
+-- module. It is in this module so that you can use it from places like the
+-- typeclass solver itself, to avoid a module import cycle (since the regular
+-- 'Cryptol.TypeCheck.Subst.apSubst' has to import the class solver to do the
+-- substitution).
+module Cryptol.TypeCheck.Subst.Type
+  ( Subst(..)
+  , emptySubst
+  , SubstError(..)
+  , singleSubst
+  , singleTParamSubst
+  , uncheckedSingleSubst
+  , defaultingSubst
+  , listSubst
+  , listParamSubst
+  , isEmptySubst
+  , substBinds
+  , substToList
+  , mergeDistinctSubst
+  , apSubstMaybe'
+  , applySubstToVar'
+  , apSubstNoSimp
+  ) where
+
+import           Data.Maybe
+import           Data.Either (partitionEithers)
+import qualified Data.IntMap as IntMap
+import           Data.Set (Set)
+import qualified Data.Set as Set
+
+import Cryptol.TypeCheck.AST
+import Cryptol.TypeCheck.PP
+import qualified Cryptol.TypeCheck.SimpType as Simp
+import Cryptol.Utils.Panic (panic)
+import Cryptol.Utils.Misc (anyJust, anyJust2, anyJust3)
+
+-- | A 'Subst' value represents a substitution that maps each 'TVar'
+-- to a 'Type'.
+--
+-- Invariant 1: If there is a mapping from @TVFree _ _ tps _@ to a
+-- type @t@, then @t@ must not mention (directly or indirectly) any
+-- type parameter that is not in @tps@. In particular, if @t@ contains
+-- a variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
+-- @tps@. This ensures that applying the substitution will not permit
+-- any type parameter to escape from its scope.
+--
+-- Invariant 2: The substitution must be idempotent, in that applying
+-- a substitution to any 'Type' in the map should leave that 'Type'
+-- unchanged. In other words, 'Type' values in the range of a 'Subst'
+-- should not mention any 'TVar' in the domain of the 'Subst'. In
+-- particular, this implies that a substitution must not contain any
+-- recursive variable mappings.
+--
+-- Invariant 3: The substitution must be kind correct: Each 'TVar' in
+-- the substitution must map to a 'Type' of the same kind.
+
+data Subst = S { suFreeMap :: !(IntMap.IntMap (TVar, Type))
+               , suBoundMap :: !(IntMap.IntMap (TVar, Type))
+               , suDefaulting :: !Bool
+               }
+                  deriving Show
+
+emptySubst :: Subst
+emptySubst =
+  S { suFreeMap = IntMap.empty
+    , suBoundMap = IntMap.empty
+    , suDefaulting = False
+    }
+
+mergeDistinctSubst :: [Subst] -> Subst
+mergeDistinctSubst sus =
+  case sus of
+    [] -> emptySubst
+    _  -> foldr1 merge sus
+
+  where
+  merge s1 s2 = S { suFreeMap     = jn suFreeMap s1 s2
+                  , suBoundMap    = jn suBoundMap s1 s2
+                  , suDefaulting  = if suDefaulting s1 || suDefaulting s2
+                                      then err
+                                      else False
+                  }
+
+  err       = panic "mergeDistinctSubst" [ "Not distinct" ]
+  bad _ _   = err
+  jn f x y  = IntMap.unionWith bad (f x) (f y)
+
+
+
+
+
+
+-- | Reasons to reject a single-variable substitution.
+data SubstError
+  = SubstRecursive
+  -- ^ 'TVar' maps to a type containing the same variable.
+  | SubstEscaped [TParam]
+  -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.
+  | SubstKindMismatch Kind Kind
+  -- ^ 'TVar' maps to a type with a different kind.
+
+singleSubst :: TVar -> Type -> Either SubstError Subst
+singleSubst x t
+  | kindOf x /= kindOf t   = Left (SubstKindMismatch (kindOf x) (kindOf t))
+  | x `Set.member` fvs t   = Left SubstRecursive
+  | not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped))
+  | otherwise              = Right (uncheckedSingleSubst x t)
+  where
+    escaped =
+      case x of
+        TVBound _ -> Set.empty
+        TVFree _ _ scope _ -> freeParams t `Set.difference` scope
+
+uncheckedSingleSubst :: TVar -> Type -> Subst
+uncheckedSingleSubst v@(TVFree i _ _tps _) t =
+  S { suFreeMap = IntMap.singleton i (v, t)
+    , suBoundMap = IntMap.empty
+    , suDefaulting = False
+    }
+uncheckedSingleSubst v@(TVBound tp) t =
+  S { suFreeMap = IntMap.empty
+    , suBoundMap = IntMap.singleton (tpUnique tp) (v, t)
+    , suDefaulting = False
+    }
+
+singleTParamSubst :: TParam -> Type -> Subst
+singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t
+
+-- | A defaulting substitution maps all otherwise-unmapped free
+-- variables to a kind-appropriate default type (@Bit@ for value types
+-- and @0@ for numeric types).
+defaultingSubst :: Subst -> Subst
+defaultingSubst s = s { suDefaulting = True }
+
+-- | Makes a substitution out of a list.
+-- WARNING: We do not validate the list in any way, so the caller should
+-- ensure that we end up with a valid (e.g., idempotent) substitution.
+listSubst :: [(TVar, Type)] -> Subst
+listSubst xs
+  | null xs   = emptySubst
+  | otherwise = S { suFreeMap = IntMap.fromList frees
+                  , suBoundMap = IntMap.fromList bounds
+                  , suDefaulting = False }
+  where
+    (frees, bounds) = partitionEithers (map classify xs)
+    classify x =
+      case fst x of
+        TVFree i _ _ _ -> Left (i, x)
+        TVBound tp -> Right (tpUnique tp, x)
+
+-- | Makes a substitution out of a list.
+-- WARNING: We do not validate the list in any way, so the caller should
+-- ensure that we end up with a valid (e.g., idempotent) substitution.
+listParamSubst :: [(TParam, Type)] -> Subst
+listParamSubst xs
+  | null xs   = emptySubst
+  | otherwise = S { suFreeMap = IntMap.empty
+                  , suBoundMap = IntMap.fromList bounds
+                  , suDefaulting = False }
+  where
+    bounds = [ (tpUnique tp, (TVBound tp, t)) | (tp, t) <- xs ]
+
+isEmptySubst :: Subst -> Bool
+isEmptySubst su = IntMap.null (suFreeMap su) && IntMap.null (suBoundMap su)
+
+-- Returns the empty set if this is a defaulting substitution
+substBinds :: Subst -> Set TVar
+substBinds su
+  | suDefaulting su = Set.empty
+  | otherwise       = Set.fromList (map fst (assocsSubst su))
+
+substToList :: Subst -> [(TVar, Type)]
+substToList s
+  | suDefaulting s = panic "substToList" ["Defaulting substitution."]
+  | otherwise = assocsSubst s
+
+assocsSubst :: Subst -> [(TVar, Type)]
+assocsSubst s = frees ++ bounds
+  where
+    frees = IntMap.elems (suFreeMap s)
+    bounds = IntMap.elems (suBoundMap s)
+
+instance PP (WithNames Subst) where
+  ppPrec _ (WithNames s mp)
+    | null els  = text "(empty substitution)"
+    | otherwise = text "Substitution:" $$ nest 2 (vcat (map pp1 els))
+    where pp1 (x,t) = ppWithNames mp x <+> text "=" <+> ppWithNames mp t
+          els       = assocsSubst s
+
+instance PP Subst where
+  ppPrec n = ppWithNamesPrec IntMap.empty n
+
+-- | Apply a substitution.  Returns `Nothing` if nothing changed.
+-- The @Prop -> Prop@ function is how to simplify the result if it is a
+-- predicate.
+apSubstMaybe' :: (Prop -> Prop) -> Subst -> Type -> Maybe Type
+apSubstMaybe' simpProp su ty =
+  case ty of
+    TCon t ts ->
+      do ss <- anyJust (apSubstMaybe' simpProp su) ts
+         case t of
+           TF _ -> Just $! Simp.tCon t ss
+           PC _ -> Just $! simpProp (TCon t ss)
+           _    -> Just (TCon t ss)
+
+    TUser f ts t ->
+      do (ts1, t1) <- anyJust2 (anyJust (apSubstMaybe' simpProp su))
+                               (apSubstMaybe' simpProp su)
+                               (ts, t)
+         Just (TUser f ts1 t1)
+
+    TRec fs -> TRec `fmap` (anyJust (apSubstMaybe' simpProp su) fs)
+
+    {- We apply the substitution to nominal types as well, because it might
+    contain module parameters, which need to be substituted when
+    instantiating a functor. -}
+    TNominal nt ts ->
+      uncurry TNominal <$> anyJust2 (applySubstToNominalType' simpProp su)
+                                    (anyJust (apSubstMaybe' simpProp su))
+                                    (nt,ts)
+
+    TVar x -> applySubstToVar' (apSubstMaybe' simpProp) su x
+
+-- | Apply a substitution without simplifying the result when it is a predicate.
+--
+-- This is used by the typeclass solver itself, if it needs to perform
+-- substitution; e.g., when solving derived instances for nominal types. Some
+-- code asks the typeclass solver to do only a single simplification step; if it
+-- called the regular 'Cryptol.TypeCheck.Subst.apSubst' which simplifies
+-- recursively after substitution, then it would do many simplification steps
+-- instead of one, resulting in worse error messages. Not doing simplification
+-- also allows us to avoid a module dependency cycle.
+apSubstNoSimp :: Subst -> Type -> Type
+apSubstNoSimp su ty = fromMaybe ty (apSubstMaybe' id su ty)
+
+lookupSubst :: TVar -> Subst -> Maybe Type
+lookupSubst x su =
+  fmap snd $
+  case x of
+    TVFree i _ _ _ -> IntMap.lookup i (suFreeMap su)
+    TVBound tp -> IntMap.lookup (tpUnique tp) (suBoundMap su)
+
+applySubstToVar' :: (Subst -> Type -> Maybe Type) -> Subst -> TVar -> Maybe Type
+applySubstToVar' substType su x =
+  case lookupSubst x su of
+    -- For a defaulting substitution, we must recurse in order to
+    -- replace unmapped free vars with default types.
+    Just t
+      | suDefaulting su -> Just $! fromMaybe t (substType su t)
+      | otherwise       -> Just t
+    Nothing
+      | suDefaulting su -> Just $! defaultFreeVar x
+      | otherwise       -> Nothing
+
+applySubstToNominalType' :: (Prop -> Prop)
+                         -> Subst -> NominalType -> Maybe NominalType
+applySubstToNominalType' simpProp su nt =
+ do (cs,def,der) <- anyJust3 (anyJust (apSubstMaybe' simpProp su))
+                             apSubstDef
+                             (anyJust (anyJust (apSubstMaybe' simpProp su)))
+                             (ntConstraints nt, ntDef nt, ntDeriving nt)
+    pure nt { ntConstraints = cs, ntDef = def, ntDeriving = der }
+  where
+  apSubstDef d =
+    case d of
+      Struct c ->
+        do fs <- anyJust (apSubstMaybe' simpProp su) (ntFields c)
+           pure (Struct c { ntFields = fs })
+      Enum cs -> Enum <$> anyJust apSubstCon cs
+      Abstract -> pure Abstract
+
+  apSubstCon c =
+    do fs <- anyJust (apSubstMaybe' simpProp su) (ecFields c)
+       pure c { ecFields = fs }
+
+-- | Pick types for unconstrained unification variables.
+defaultFreeVar :: TVar -> Type
+defaultFreeVar x@(TVBound {}) = TVar x
+defaultFreeVar (TVFree _ k _ d) =
+  case k of
+    KType -> tBit
+    KNum  -> tNum (0 :: Int)
+    _     -> panic "Cryptol.TypeCheck.Subst.defaultFreeVar"
+                  [ "Free variable of unexpected kind."
+                  , "Source: " ++ show d
+                  , "Kind: " ++ show (pp k) ]
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
@@ -327,6 +327,13 @@
   , ntKind        :: !Kind             -- ^ Result kind
   , ntConstraints :: [Prop]
   , ntDef         :: NominalTypeDef
+  , ntDeriving    :: Map PC [Prop]
+    -- ^ Derived classes and their conditions (which may contain type
+    -- variables).
+    --
+    -- For instance, if we have @enum Maybe a = Nothing | Just a deriving (Eq)@,
+    -- this map would be @{Eq -> [Eq a]}@, since the derived instance is
+    -- @instance (Eq a) => Eq (Maybe a)@.
   , ntFixity      :: !(Maybe Fixity)
   , ntDoc         :: Maybe Text
   } deriving (Show, Generic, NFData)
@@ -456,9 +463,17 @@
 superclassSet (TCon (PC PPrime) [n]) =
   Set.fromList [ pFin n, n >== tTwo ]
 
-superclassSet (TCon (PC p0) [t]) = go p0
+superclassSet (TCon (PC p0) [t]) =
+  Set.map (\p -> TCon (PC p) [t]) (typeSuperclassSet p0)
+
+superclassSet _ = mempty
+
+-- | Given a typeclass of kind @* -> Prop@, compute the set of all transitive
+-- superclasses of kind @* -> Prop@.
+typeSuperclassSet :: PC -> Set PC
+typeSuperclassSet = go
   where
-  super p = Set.insert (TCon (PC p) [t]) (go p)
+  super p = Set.insert p (go p)
 
   go PRing      = super PZero
   go PLogic     = super PZero
@@ -468,8 +483,6 @@
   go PCmp       = super PEq
   go PSignedCmp = super PEq
   go _ = mempty
-
-superclassSet _ = mempty
 
 
 nominalTypeConTypes :: NominalType -> [(Name,Schema)]
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
@@ -13,6 +13,7 @@
   , aLiteral
   , aLiteralLessThan
   , aLogic
+  , aIntegral
 
   , aTVar
   , aFreeTVar
@@ -191,6 +192,9 @@
 
 aLogic :: Pat Prop Type
 aLogic = tp PLogic ar1
+
+aIntegral :: Pat Prop Type
+aIntegral = tp PIntegral ar1
 
 --------------------------------------------------------------------------------
 anError :: Kind -> Pat Type ()
diff --git a/src/Cryptol/Utils/Misc.hs b/src/Cryptol/Utils/Misc.hs
--- a/src/Cryptol/Utils/Misc.hs
+++ b/src/Cryptol/Utils/Misc.hs
@@ -34,3 +34,11 @@
     (Just x , Nothing) -> Just (x, b)
     (Nothing, Just y ) -> Just (a, y)
     (Just x , Just y ) -> Just (x, y)
+
+-- | Apply functions to all 3 elements of a triple.
+-- Returns 'Nothing' if nothing changed, and @Just triple@ otherwise.
+anyJust3 :: (a -> Maybe a) -> (b -> Maybe b) -> (c -> Maybe c)
+         -> (a, b, c) -> Maybe (a, b, c)
+anyJust3 f g h (a, b, c) = do
+  (a', (b', c')) <- anyJust2 f (anyJust2 g h) (a, (b, c))
+  pure (a', b', c')