diff --git a/src/Cryptol/Parser/Unlit.hs b/src/Cryptol/Parser/Unlit.hs
index 548fc2e9..03ca501f 100644
--- a/src/Cryptol/Parser/Unlit.hs
+++ b/src/Cryptol/Parser/Unlit.hs
@@ -18,6 +18,8 @@ import qualified Data.Text.Lazy as Text
 import           Data.Char(isSpace)
 import           System.FilePath(takeExtension)
 
+import           Cryptol.Utils.Panic
+
 data PreProc = None | Markdown | LaTeX
 
 knownExts :: [String]
@@ -59,7 +61,7 @@ toCryptol (Comment ls) =
                  in "/* " `Text.append` l1 : more ++ [ l `Text.append` " */" ]
 
   where
-  splitLast []  = error "splitLats []"
+  splitLast []  = panic "Cryptol.Parser.Unlit.toCryptol" [ "splitLast []" ]
   splitLast [x] = ([], x)
   splitLast (x : xs) = let (ys,y) = splitLast xs
                        in (x:ys,y)
diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs
index 2bc68b57..82f040c8 100644
--- a/src/Cryptol/Prims/Eval.hs
+++ b/src/Cryptol/Prims/Eval.hs
@@ -36,14 +36,16 @@ import System.Random (mkStdGen)
 -- Utilities -------------------------------------------------------------------
 
 #if __GLASGOW_HASKELL__ < 706
+noNum = panic "Cryptol.Prims.Eval"
+          [ "Num instance for Bool shouldn't be used." ]
 instance Num Bool where
-  _ + _         = error "Num instance for Bool shouldn't be used."
-  _ * _         = error "Num instance for Bool shouldn't be used."
-  _ - _         = error "Num instance for Bool shouldn't be used."
-  negate _      = error "Num instance for Bool shouldn't be used."
-  abs _         = error "Num instance for Bool shouldn't be used."
-  signum _      = error "Num instance for Bool shouldn't be used."
-  fromInteger _ = error "Num instance for Bool shouldn't be used."
+  _ + _         = noNum
+  _ * _         = noNum
+  _ - _         = noNum
+  negate _      = noNum
+  abs _         = noNum
+  signum _      = noNum
+  fromInteger _ = noNum
 #endif
 
 #if __GLASGOW_HASKELL__ < 708
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
index 62be4b5d..0e3e1639 100644
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -55,7 +55,8 @@ lookupProver :: String -> SBV.SMTConfig
 lookupProver s =
   case lookup s proverConfigs of
     Just cfg -> cfg
-    Nothing  -> error $ "invalid prover: " ++ s
+    -- should be caught by UI for setting prover user variable
+    Nothing  -> panic "Cryptol.Symbolic" [ "invalid prover: " ++ s ]
 
 -- | A prover result is either an error message, or potentially a
 -- counterexample or satisfying assignment.
@@ -141,12 +142,12 @@ parseValues (t : ts) cws = (v : vs, cws'')
         (vs, cws'') = parseValues ts cws'
 
 parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW])
-parseValue FTBit [] = error "parseValue"
+parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
 parseValue FTBit (cw : cws) = (Eval.VBit (SBV.fromCW cw), cws)
 parseValue (FTSeq 0 FTBit) cws = (Eval.VWord (Eval.BV 0 0), cws)
 parseValue (FTSeq n FTBit) (cw : cws)
   | SBV.isBounded cw = (Eval.VWord (Eval.BV (toInteger n) (SBV.fromCW cw)), cws)
-  | otherwise = error "parseValue"
+  | otherwise = panic "Cryptol.Symbolic.parseValue" [ "unbounded concrete word" ]
 parseValue (FTSeq n FTBit) cws = (Eval.VSeq True vs, cws')
   where (vs, cws') = parseValues (replicate n FTBit) cws
 parseValue (FTSeq n t) cws = (Eval.VSeq False vs, cws')
diff --git a/src/Cryptol/Symbolic/BitVector.hs b/src/Cryptol/Symbolic/BitVector.hs
index 0d49f21b..e63bd893 100644
--- a/src/Cryptol/Symbolic/BitVector.hs
+++ b/src/Cryptol/Symbolic/BitVector.hs
@@ -21,6 +21,8 @@ import Data.SBV.Bridge.Yices
 import Data.SBV.Internals
 import Data.SBV.BitVectors.Data
 
+import Cryptol.Utils.Panic
+
 -- BitVector type --------------------------------------------------------------
 
 data BitVector = BV { signedcxt :: Bool, width :: !Int, val :: !Integer }
@@ -46,7 +48,9 @@ signed w x
   | otherwise                  = x
 
 same :: Int -> Int -> Int
-same m n = if m == n then m else error $ "BitVector size mismatch: " ++ show (m, n)
+same m n | m == n = m
+         | otherwise = panic "Cryptol.Symbolic.BitVector.same"
+                         [ "BitVector size mismatch: " ++ show (m, n) ]
 
 instance SignCast SWord SWord where
   signCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =
@@ -56,7 +60,8 @@ instance SignCast SWord SWord where
     k = KBounded True w
     y st = do xsw <- sbvToSW st x
               newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw])
-  signCast _ = error "SignCast not called on BitVector value"
+  signCast _ = panic "Cryptol.Symbolic.BitVector"
+                 [ "signCast called on non-bitvector value" ]
   unsignCast (SBV (KBounded _ w) (Left (cwVal -> (CWInteger x)))) =
     SBV k (Left (CW k (CWInteger (unsigned w x)))) where
       k = KBounded False w
@@ -64,9 +69,12 @@ instance SignCast SWord SWord where
     k = KBounded False w
     y st = do xsw <- sbvToSW st x
               newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw])
+  unsignCast _ = panic "Cryptol.Symbolic.BitVector"
+                   [ "unsignCast called on non-bitvector value" ]
 
 instance Num BitVector where
-  fromInteger n = error $ "fromInteger " ++ show n ++ " :: BitVector"
+  fromInteger n = panic "Cryptol.Symbolic.BitVector"
+                    [ "fromInteger " ++ show n ++ " :: BitVector" ]
   BV s m x + BV _ n y = sbv s (same m n) (x + y)
   BV s m x - BV _ n y = sbv s (same m n) (x - y)
   BV s m x * BV _ n y = sbv s (same m n) (x * y)
@@ -82,7 +90,8 @@ instance Bits BitVector where
   shift (BV s m x) i           = sbv s m (shift x i)
   rotate (BV s m x) i          = sbv s m (shift x j .|. shift x (j - m))
                                   where j = i `mod` m
-  bit _i                       = error "bit: can't determine width"
+  bit _i                       = panic "Cryptol.Symbolic.BitVector"
+                                   [ "bit: can't determine width" ]
   setBit (BV s m x) i          = BV s m (setBit x i)
   clearBit (BV s m x) i        = BV s m (clearBit x i)
   complementBit (BV s m x) i   = BV s m (complementBit x i)
@@ -103,8 +112,10 @@ instance SymWord BitVector where
   literal (BV s w x) = SBV k (Left (mkConstCW k x))
       where k = KBounded s w
   fromCW c@(CW (KBounded s w) _) = BV s w (fromCW c)
-  fromCW c = error $ "fromCW: Unsupported non-integral value: " ++ show c
-  mkSymWord _ _ = error "mkSymWord unimplemented for type BitVector"
+  fromCW c = panic "Cryptol.Symbolic.BitVector"
+               [ "fromCW: Unsupported non-integral value: " ++ show c ]
+  mkSymWord _ _ = panic "Cryptol.Symbolic.BitVector"
+                    [ "mkSymWord unimplemented for type BitVector" ]
 
 instance SIntegral BitVector where
 
@@ -132,12 +143,13 @@ extract i j x@(SBV (KBounded s _) _) =
     SBV _ (Left cw) ->
       case cw of
         CW _ (CWInteger v) -> SBV k (Left (normCW (CW k (CWInteger (v `shiftR` j)))))
-        _ -> error "extract"
+        _ -> panic "Cryptol.Symbolic.BitVector.extract" [ "non-integer concrete word" ]
     _ -> SBV k (Right (cache y))
       where y st = do sw <- sbvToSW st x
                       newExpr st k (SBVApp (Extract i j) [sw])
   where
     k = KBounded s (i - j + 1)
+extract _ _ _ = panic "Cryptol.Symbolic.BitVector.extract" [ "non-bitvector value" ]
 
 cat :: SWord -> SWord -> SWord
 cat x y | bitSize x == 0 = y
@@ -146,7 +158,7 @@ cat x@(SBV _ (Left a)) y@(SBV _ (Left b)) =
   case (a, b) of
     (CW _ (CWInteger m), CW _ (CWInteger n)) ->
       SBV k (Left (CW k (CWInteger ((m `shiftL` (bitSize y) .|. n)))))
-    _ -> error "cat"
+    _ -> panic "Cryptol.Symbolic.BitVector.cat" [ "non-integer concrete word" ]
   where k = KBounded False (bitSize x + bitSize y)
 cat x y = SBV k (Right (cache z))
   where k = KBounded False (bitSize x + bitSize y)
diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs
index 90010286..293c2281 100644
--- a/src/Cryptol/Symbolic/Prims.hs
+++ b/src/Cryptol/Symbolic/Prims.hs
@@ -20,6 +20,7 @@ import Cryptol.Symbolic.BitVector
 import Cryptol.Symbolic.Value
 import Cryptol.TypeCheck.AST (Name)
 import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)
+import Cryptol.Utils.Panic
 
 import qualified Data.SBV as SBV
 import Data.SBV (SBool)
@@ -280,7 +281,8 @@ evalECon econ =
             zs = take (fromInteger j) (snd (Poly.mdp (reverse xs) (reverse ys)) ++ repeat SBV.false)
         in VSeq True (map VBit (reverse zs))
 
-    ECRandom      -> error "ECRandom"
+    ECRandom      -> panic "Cryptol.Symbolic.Prims.evalECon"
+                       [ "can't symbolically evaluae ECRandom" ]
 
 
 selectV :: (Integer -> Value) -> Value -> Value
@@ -318,14 +320,14 @@ mapV f v =
   case v of
     VSeq b xs  -> VSeq b (map f xs)
     VStream xs -> VStream (map f xs)
-    _          -> error "mapV"
+    _          -> panic "Cryptol.Symbolic.Prims.mapV" [ "non-mappable value" ]
 
 catV :: Value -> Value -> Value
 catV (VWord x)   ys           = VWord (cat x (fromWord ys))
 catV xs          (VWord y)    = VWord (cat (fromWord xs) y)
 catV (VSeq b xs) (VSeq _ ys)  = VSeq b (xs ++ ys)
 catV (VSeq _ xs) (VStream ys) = VStream (xs ++ ys)
-catV _ _ = error "catV"
+catV _ _ = panic "Cryptol.Symbolic.Prims.catV" [ "non-concatenable value" ]
 
 dropV :: Integer -> Value -> Value
 dropV 0 xs = xs
@@ -334,7 +336,7 @@ dropV n xs =
     VSeq b xs'  -> VSeq b (genericDrop n xs')
     VStream xs' -> VStream (genericDrop n xs')
     VWord w     -> VWord $ extract (bitSize w - 1 - fromInteger n) 0 w
-    _           -> error "dropV"
+    _           -> panic "Cryptol.Symbolic.Prims.dropV" [ "non-droppable value" ]
 
 takeV :: Integer -> Value -> Value
 takeV n xs =
@@ -344,7 +346,7 @@ takeV n xs =
     VStream xs' -> VSeq b (genericTake n xs')
                      where b = case xs' of VBit _ : _ -> True
                                            _          -> False
-    _           -> error "takeV"
+    _           -> panic "Cryptol.Symbolic.Prims.takeV" [ "non-takeable value" ]
 
 -- | Make a numeric constant.
 -- { val, bits } (fin val, fin bits, bits >= width val) => [bits]
@@ -379,7 +381,7 @@ toTypeVal ty
   | Just (aty, bty) <- isTFun ty = TVFun (toTypeVal aty) (toTypeVal bty)
   | Just (_, tys) <- isTTuple ty = TVTuple (map toTypeVal tys)
   | Just fields <- isTRec ty     = TVRecord [ (n, toTypeVal aty) | (n, aty) <- fields ]
-  | otherwise                    = error "internal error: bad TValue"
+  | otherwise                    = panic "Cryptol.Symbolic.Prims.toTypeVal" [ "bad TValue" ]
 
 -- Arith -----------------------------------------------------------------------
 
@@ -443,12 +445,16 @@ cmpValue fb fw = cmp
         (VBit b1    , VBit b2    ) -> fb b1 b2 k
         (VWord w1   , VWord w2   ) -> fw w1 w2 k
         (VSeq _ vs1 , VSeq _ vs2 ) -> cmpValues vs1 vs2 k
-        (VStream {} , VStream {} ) -> error "Infinite streams are not comparable"
-        (VFun {}    , VFun {}    ) -> error "Functions are not comparable"
-        (VPoly {}   , VPoly {}   ) -> error "Polymorphic values are not comparable"
+        (VStream {} , VStream {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
+                                        [ "Infinite streams are not comparable" ]
+        (VFun {}    , VFun {}    ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
+                                        [ "Functions are not comparable" ]
+        (VPoly {}   , VPoly {}   ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
+                                        [ "Polymorphic values are not comparable" ]
         (VWord w1   , _          ) -> fw w1 (fromWord v2) k
         (_          , VWord w2   ) -> fw (fromWord v1) w2 k
-        (_          , _          ) -> error "type mismatch"
+        (_          , _          ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
+                                        [ "type mismatch" ]
 
     cmpValues (x1 : xs1) (x2 : xs2) k = cmp x1 x2 (cmpValues xs1 xs2 k)
     cmpValues _ _ k = k
diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs
index 94d28d7e..fd18a82f 100644
--- a/src/Cryptol/Symbolic/Value.hs
+++ b/src/Cryptol/Symbolic/Value.hs
@@ -49,11 +49,13 @@ instance Mergeable Value where
       (VPoly f1   , VPoly f2   ) -> VPoly $ symbolicMerge c f1 f2
       (VWord w1   , _          ) -> VWord $ symbolicMerge c w1 (fromWord v2)
       (_          , VWord w2   ) -> VWord $ symbolicMerge c (fromWord v1) w2
-      (_          , _          ) -> error "symbolicMerge: incompatible values"
+      (_          , _          ) -> panic "Cryptol.Symbolic.Value"
+                                      [ "symbolicMerge: incompatible values" ]
     where
       mergeField (n1, x1) (n2, x2)
         | n1 == n2  = (n1, symbolicMerge c x1 x2)
-        | otherwise = error "symbolicMerge: incompatible values"
+        | otherwise = panic "Cryptol.Symbolic.Value"
+                        [ "symbolicMerge.mergeField: incompatible values" ]
 
 -- Big-endian Words ------------------------------------------------------------
 
diff --git a/src/Cryptol/TypeCheck/Solver/CrySAT.hs b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
index 5d57733a..d9b2d500 100644
--- a/src/Cryptol/TypeCheck/Solver/CrySAT.hs
+++ b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
@@ -29,7 +29,7 @@ import           Data.Either (partitionEithers)
 import           MonadLib
 import           Control.Applicative
 
--- import Cryptol.Utils.Debug
+import           Cryptol.Utils.Panic
 
 infixr 2 :||
 infixr 3 :&&
@@ -495,7 +495,8 @@ mkLin :: Expr -> FM SAT.Expr
 mkLin ty0 =
   cryNoInf ty0 >>= \ty ->
   case ty of
-    K Inf                  -> error "mkLin: Inf"
+    K Inf                  -> panic "Cryptol.TypeCheck.Solver.CrySAT.mkLin"
+                                [ "K Inf after cryNoInf" ]
     K (Nat n)              -> return (SAT.K n)
     Var x                  -> isFin x >> return (satVar x)
     t1 :+ t2               -> (SAT.:+)            <$> mkLin t1 <*> mkLin t2
@@ -620,7 +621,8 @@ nLg2 0  = 0
 nLg2 n  = case genLog n 2 of
             Just (x,exact) | exact     -> x
                            | otherwise -> x + 1
-            Nothing -> error "genLog returned Nothing"
+            Nothing -> panic "Cryptol.TypeCheck.Solver.CrySAT.nLg2"
+                         [ "genLog returned Nothing" ]
 
 
 
diff --git a/src/Cryptol/TypeCheck/Solver/InfNat.hs b/src/Cryptol/TypeCheck/Solver/InfNat.hs
index 7e6b0a68..9f7e2500 100644
--- a/src/Cryptol/TypeCheck/Solver/InfNat.hs
+++ b/src/Cryptol/TypeCheck/Solver/InfNat.hs
@@ -12,6 +12,8 @@
 {-# LANGUAGE Safe #-}
 module Cryptol.TypeCheck.Solver.InfNat where
 
+import Cryptol.Utils.Panic
+
 -- | Natural numbers with an infinity element
 data Nat' = Nat Integer | Inf
             deriving (Show,Eq,Ord)
@@ -109,7 +111,8 @@ nLg2 (Nat 0)  = Nat 0
 nLg2 (Nat n)  = case genLog n 2 of
                   Just (x,exact) | exact     -> Nat x
                                  | otherwise -> Nat (x + 1)
-                  Nothing -> error "genLog returned Nothing"
+                  Nothing -> panic "Cryptol.TypeCheck.Solver.InfNat.nLg2"
+                               [ "genLog returned Nothing" ]
 
 -- | @nWidth n@ is number of bits needed to represent all numbers
 -- from 0 to n, inclusive. @nWidth x = nLg2 (x + 1)@.
@@ -118,7 +121,8 @@ nWidth Inf      = Inf
 nWidth (Nat 0)  = Nat 0
 nWidth (Nat n)  = case genLog n 2 of
                     Just (x,_) -> Nat (x + 1)
-                    Nothing -> error "genLog returned Nothing"
+                    Nothing -> panic "Cryptol.TypeCheck.Solver.InfNat.nWidth"
+                                 [ "genLog returned Nothing" ]
 
 
 nLenFromThen :: Nat' -> Nat' -> Nat' -> Maybe Nat'
diff --git a/src/Cryptol/TypeCheck/TypeOf.hs b/src/Cryptol/TypeCheck/TypeOf.hs
index d7f12277..a65faae7 100644
--- a/src/Cryptol/TypeCheck/TypeOf.hs
+++ b/src/Cryptol/TypeCheck/TypeOf.hs
@@ -16,6 +16,8 @@ module Cryptol.TypeCheck.TypeOf
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Subst
 import Cryptol.Prims.Types (typeOf)
+import Cryptol.Utils.Panic
+import Cryptol.Utils.PP
 
 import           Data.Map    (Map)
 import qualified Data.Map as Map
@@ -37,7 +39,8 @@ fastTypeOf tyenv expr =
     EAbs x t e    -> tFun t (fastTypeOf (Map.insert x (Forall [] [] t) tyenv) e)
     EApp e _      -> case tIsFun (fastTypeOf tyenv e) of
                         Just (_, t) -> t
-                        Nothing     -> error "internal error"
+                        Nothing     -> panic "Cryptol.TypeCheck.TypeOf.fastTypeOf"
+                                         [ "EApp with non-function operator" ]
     ECast _ t     -> t
     -- Polymorphic fragment
     ECon      {}  -> polymorphic
@@ -51,7 +54,8 @@ fastTypeOf tyenv expr =
     polymorphic =
       case fastSchemaOf tyenv expr of
         Forall [] [] ty -> ty
-        _ -> error "internal error: unexpected polymorphic type"
+        _ -> panic "Cryptol.TypeCheck.TypeOf.fastTypeOf"
+               [ "unexpected polymorphic type" ]
 
 fastSchemaOf :: Map QName Schema -> Expr -> Schema
 fastSchemaOf tyenv expr =
@@ -64,13 +68,18 @@ fastSchemaOf tyenv expr =
     ETApp e t      -> case fastSchemaOf tyenv e of
                         Forall (tparam : tparams) props ty -> Forall tparams (apSubst s props) (apSubst s ty)
                                                                 where s = singleSubst (tpVar tparam) t
-                        _ -> error "internal error"
+                        _ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
+                               [ "ETApp body with no type parameters" ]
     EProofAbs p e  -> case fastSchemaOf tyenv e of
                         Forall [] props ty -> Forall [] (p : props) ty
-                        _ -> error "internal error"
+                        _ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
+                               [ "EProofAbs with polymorphic expression" ]
     EProofApp e    -> case fastSchemaOf tyenv e of
                         Forall [] (_ : props) ty -> Forall [] props ty
-                        _ -> error "internal error"
+                        _ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
+                               [ "EProofApp with polymorphic expression or"
+                               , "no props in scope"
+                               ]
     EWhere e dgs   -> fastSchemaOf (foldr addDeclGroup tyenv dgs) e
                         where addDeclGroup (Recursive ds) = flip (foldr addDecl) ds
                               addDeclGroup (NonRecursive d) = addDecl d
@@ -93,4 +102,5 @@ typeSelect :: Type -> Selector -> Type
 typeSelect (TCon _tctuple ts) (TupleSel i _) = ts !! (i - 1)
 typeSelect (TRec fields) (RecordSel n _) = fromJust (lookup n fields)
 typeSelect (TCon _tcseq [_, a]) (ListSel _ _) = a
-typeSelect _ _ = error "internal error: typeSelect"
+typeSelect ty _ = panic "Cryptol.TypeCheck.TypeOf.typeSelect"
+                    [ "cannot apply selector to value of type", render (pp ty) ]