Make a separate ADT case for each user-facing error message.

This is preparation for giving better source information in error messages.

27 files changed, 506 insertions, 360 deletions

diff --git a/src/dex.hs b/src/dex.hs
index 623c2bde..f8bce647 100644
--- a/src/dex.hs
+++ b/src/dex.hs
@@ -32,6 +32,7 @@ import ConcreteSyntax (keyWordStrs, preludeImportBlock)
 import RenderHtml
 -- import Live.Terminal (runTerminal)
 import Live.Web (runWeb)
+import PPrint  hiding (hardline)
 import Core
 import Types.Core
 import Types.Imp
diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs
index a21062ff..6a4b2584 100644
--- a/src/lib/AbstractSyntax.hs
+++ b/src/lib/AbstractSyntax.hs
@@ -58,7 +58,7 @@ import Data.Text (Text)
 import ConcreteSyntax
 import Err
 import Name
-import PPrint ()
+import PPrint
 import Types.Primitives
 import Types.Source
 import qualified Types.OpNames as P
@@ -139,7 +139,7 @@ decl ann (WithSrcs sid _ d) = WithSrcB sid <$> case d of
   CLet binder rhs -> do
     (p, ty) <- patOptAnn binder
     ULet ann p ty <$> asExpr <$> block rhs
-  CBind _ _ -> throw SyntaxErr "Arrow binder syntax <- not permitted at the top level, because the binding would have unbounded scope."
+  CBind _ _ -> throw TopLevelArrowBinder
   CDefDecl def -> do
     (name, lam) <- aDef def
     return $ ULet ann (fromSourceNameW name) Nothing (WithSrcE sid (ULam lam))
@@ -199,7 +199,7 @@ withTrailingConstraints g cont = case g of
     Nest (UAnnBinder expl (WithSrcB sid b) ann cs) bs <- withTrailingConstraints lhs cont
     s <- case b of
       UBindSource s -> return s
-      UIgnore       -> throw SyntaxErr "Can't constrain anonymous binders"
+      UIgnore       -> throw CantConstrainAnonBinders
       UBind _ _     -> error "Shouldn't have internal names until renaming pass"
     c' <- expr c
     return $   UnaryNest (UAnnBinder expl (WithSrcB sid b) ann (cs ++ [c']))
@@ -261,7 +261,7 @@ uBinder :: GroupW -> SyntaxM (UBinder c VoidS VoidS)
 uBinder (WithSrcs sid _ b) = case b of
   CLeaf (CIdentifier name) -> return $ fromSourceNameW $ WithSrc sid name
   CLeaf CHole -> return $ WithSrcB sid UIgnore
-  _ -> throw SyntaxErr "Binder must be an identifier or `_`"
+  _ -> throw UnexpectedBinder
 
 -- Type annotation with an optional binder pattern
 tyOptPat :: GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
@@ -300,8 +300,7 @@ pat (WithSrcs sid _ grp) = WithSrcB sid <$> case grp of
   CLeaf (CIdentifier name) -> return $ UPatBinder $ fromSourceNameW $ WithSrc sid name
   CJuxtapose True lhs rhs -> do
     case lhs of
-      WithSrcs _ _ (CJuxtapose True _ _) ->
-        throw SyntaxErr "Only unary constructors can form patterns without parens"
+      WithSrcs _ _ (CJuxtapose True _ _) -> throw OnlyUnaryWithoutParens
       _ -> return ()
     name <- identifier "pattern constructor name" lhs
     arg <- pat rhs
@@ -313,11 +312,11 @@ pat (WithSrcs sid _ grp) = WithSrcB sid <$> case grp of
         gs' <- mapM pat gs
         return $ UPatCon (fromSourceNameW name) (toNest gs')
       _ -> error "unexpected postfix group (should be ruled out at grouping stage)"
-  _ -> throw SyntaxErr "Illegal pattern"
+  _ -> throw IllegalPattern
 
 tyOptBinder :: Explicitness -> GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
 tyOptBinder expl (WithSrcs sid sids grp) = case grp of
-  CBin (WithSrc _ Pipe)  _ _     -> throw SyntaxErr "Unexpected constraint"
+  CBin (WithSrc _ Pipe)  _ _     -> throw UnexpectedConstraint
   CBin (WithSrc _ Colon) name ty -> do
     b <- uBinder name
     ann <- UAnn <$> expr ty
@@ -341,7 +340,7 @@ binderReqTy expl (WithSrcs _ _ (CBin (WithSrc _ Colon) name ty)) = do
   b <- uBinder name
   ann <- UAnn <$> expr ty
   return $ UAnnBinder expl b ann []
-binderReqTy _ _ = throw SyntaxErr $ "Expected an annotated binder"
+binderReqTy _ _ = throw ExpectedAnnBinder
 
 argList :: [GroupW] -> SyntaxM ([UExpr VoidS], [UNamedArg VoidS])
 argList gs = partitionEithers <$> mapM singleArg gs
@@ -355,7 +354,7 @@ singleArg = \case
 identifier :: String -> GroupW -> SyntaxM SourceNameW
 identifier ctx (WithSrcs sid _ g) = case g of
   CLeaf (CIdentifier name) -> return $ WithSrc sid name
-  _ -> throw SyntaxErr $ "Expected " ++ ctx ++ " to be an identifier"
+  _ -> throw $ ExpectedIdentifier ctx
 
 aEffects :: WithSrcs ([GroupW], Maybe GroupW) -> SyntaxM (UEffectRow VoidS)
 aEffects (WithSrcs _ _ (effs, optEffTail)) = do
@@ -375,7 +374,7 @@ effect (WithSrcs _ _ grp) = case grp of
     return $ URWSEffect State $ fromSourceNameW (WithSrc sid h)
   CLeaf (CIdentifier "Except") -> return UExceptionEffect
   CLeaf (CIdentifier "IO"    ) -> return UIOEffect
-  _ -> throw SyntaxErr "Unexpected effect form; expected one of `Read h`, `Accum h`, `State h`, `Except`, `IO`, or the name of a user-defined effect."
+  _ -> throw UnexpectedEffectForm
 
 aMethod :: CSDeclW -> SyntaxM (Maybe (UMethodDef VoidS))
 aMethod (WithSrcs _ _ CPass) = return Nothing
@@ -386,7 +385,7 @@ aMethod (WithSrcs src _ d) = Just . WithSrcE src <$> case d of
   CLet (WithSrcs sid _ (CLeaf (CIdentifier name))) rhs -> do
     rhs' <- ULamExpr Empty ImplicitApp Nothing Nothing <$> block rhs
     return $ UMethodDef (fromSourceNameW (WithSrc sid name)) rhs'
-  _ -> throw SyntaxErr "Unexpected method definition. Expected `def` or `x = ...`."
+  _ -> throw UnexpectedMethodDef
 
 asExpr :: UBlock VoidS -> UExpr VoidS
 asExpr (WithSrcE src b) = case b of
@@ -403,7 +402,7 @@ blockDecls :: [CSDeclW] -> SyntaxM (Nest UDecl VoidS VoidS, UExpr VoidS)
 blockDecls [] = error "shouldn't have empty list of decls"
 blockDecls [WithSrcs _ _ d] = case d of
   CExpr g -> (Empty,) <$> expr g
-  _ -> throw SyntaxErr "Block must end in expression"
+  _ -> throw BlockWithoutFinalExpr
 blockDecls (WithSrcs sid _ (CBind b rhs):ds) = do
   b' <- binderOptTy Explicit b
   rhs' <- asExpr <$> block rhs
@@ -428,7 +427,7 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
   -- Table constructors here.  Other uses of square brackets
   -- should be detected upstream, before calling expr.
   CBrackets gs -> UTabCon <$> mapM expr gs
-  CGivens _ -> throw SyntaxErr $ "Unexpected `given` clause"
+  CGivens _ -> throw UnexpectedGivenClause
   CArrow lhs effs rhs -> do
     case lhs of
       WithSrcs _ _ (CParens gs) -> do
@@ -436,7 +435,7 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
         effs' <- fromMaybeM effs UPure aEffects
         resultTy <- expr rhs
         return $ UPi $ UPiExpr bs ExplicitApp effs' resultTy
-      _ -> throw SyntaxErr "Argument types should be in parentheses"
+      _ -> throw ArgsShouldHaveParens
   CDo b -> UDo <$> block b
   CJuxtapose hasSpace lhs rhs -> case hasSpace of
     True -> extendAppRight <$> expr lhs <*> expr rhs
@@ -459,7 +458,7 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
       name <- case rhs' of
         CLeaf (CIdentifier name) -> return $ FieldName name
         CLeaf (CNat i          ) -> return $ FieldNum $ fromIntegral i
-        _ -> throw SyntaxErr "Field must be a name or an integer"
+        _ -> throw BadField
       return $ UFieldAccess lhs' (WithSrc src name)
     DoubleColon   -> UTypeAnn <$> (expr lhs) <*> expr rhs
     EvalBinOp s -> evalOp s
@@ -467,14 +466,14 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
       lhs' <- tyOptPat lhs
       UDepPairTy . (UDepPairType ExplicitDepPair lhs') <$> expr rhs
     DepComma      -> UDepPair <$> (expr lhs) <*> expr rhs
-    CSEqual       -> throw SyntaxErr "Equal sign must be used as a separator for labels or binders, not a standalone operator"
-    Colon         -> throw SyntaxErr "Colon separates binders from their type annotations, is not a standalone operator.\nIf you are trying to write a dependent type, use parens: (i:Fin 4) => (..i)"
+    CSEqual       -> throw BadEqualSign
+    Colon         -> throw BadColon
     ImplicitArrow -> case lhs of
       WithSrcs _ _ (CParens gs) -> do
         bs <- aPiBinders gs
         resultTy <- expr rhs
         return $ UPi $ UPiExpr bs ImplicitApp UPure resultTy
-      _ -> throw SyntaxErr "Argument types should be in parentheses"
+      _ -> throw ArgsShouldHaveParens
     FatArrow      -> do
       lhs' <- tyOptPat lhs
       UTabPi . (UTabPiExpr lhs') <$> expr rhs
@@ -496,7 +495,7 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
         WithSrcE _ (UIntLit   i) -> UIntLit   (-i)
         WithSrcE _ (UFloatLit i) -> UFloatLit (-i)
         e -> unaryApp (mkUVar sid "neg") e
-      _ -> throw SyntaxErr $ "Prefix (" ++ pprint name ++ ") not legal as a bare expression"
+      _ -> throw $ BadPrefix $ pprint name
   CLambda params body -> do
     params' <- explicitBindersOptAnn $ WithSrcs sid [] $ map stripParens params
     body' <- block body
diff --git a/src/lib/Algebra.hs b/src/lib/Algebra.hs
index 5ecc05f7..1175d152 100644
--- a/src/lib/Algebra.hs
+++ b/src/lib/Algebra.hs
@@ -27,6 +27,7 @@ import MTL1
 import Name
 import Subst
 import QueryType
+import PPrint
 import Types.Core
 import Types.Imp
 import Types.Primitives
@@ -55,7 +56,7 @@ sumUsingPolys lim (Abs i body) = do
   sumAbs <- refreshAbs (Abs i body) \(i':>_) body' -> do
     exprAsPoly body' >>= \case
       Just poly' -> return $ Abs i' poly'
-      Nothing -> throw NotImplementedErr $
+      Nothing -> throwInternal $
         "Algebraic simplification failed to model index computations:\n"
         ++ "Trying to sum from 0 to " ++ pprint lim ++ " - 1, \\"
         ++ pprint i' ++ "." ++ pprint body'
diff --git a/src/lib/Builder.hs b/src/lib/Builder.hs
index 7415cec7..f3f790f0 100644
--- a/src/lib/Builder.hs
+++ b/src/lib/Builder.hs
@@ -17,7 +17,6 @@ import Control.Monad.State.Strict (MonadState (..), StateT (..), runStateT)
 import qualified Data.Map.Strict as M
 import Data.Foldable (fold)
 import Data.Graph (graphFromEdges, topSort)
-import Data.Text.Prettyprint.Doc (Pretty (..))
 import Foreign.Ptr
 
 import qualified Unsafe.Coerce as TrulyUnsafe
@@ -30,6 +29,7 @@ import MTL1
 import Subst
 import Name
 import PeepholeOptimize
+import PPrint
 import QueryType
 import Types.Core
 import Types.Imp
@@ -103,18 +103,6 @@ buildScopedAssumeNoDecls cont = do
     _ -> error "Expected no decl emissions"
 {-# INLINE buildScopedAssumeNoDecls #-}
 
-withReducibleEmissions
-  :: (ScopableBuilder r m, Builder r m, HasNamesE e, SubstE AtomSubstVal e)
-  => String
-  -> (forall o' . (Emits o', DExt o o') => m o' (e o'))
-  -> m o (e o)
-withReducibleEmissions msg cont = do
-  withDecls <- buildScoped cont
-  reduceWithDecls withDecls >>= \case
-    Just t -> return t
-    _ -> throw TypeErr msg
-{-# INLINE withReducibleEmissions #-}
-
 -- === "Hoisting" top-level builder class ===
 
 -- `emitHoistedEnv` lets you emit top env fragments, like cache entries or
@@ -926,10 +914,10 @@ symbolicTangentTy elTy = lookupSourceMap "SymbolicTangent" >>= \case
   Just (UTyConVar symTanName) -> do
     return $ toType $ UserADTType "SymbolicTangent" symTanName $
       TyConParams [Explicit] [toAtom elTy]
-  Nothing -> throw UnboundVarErr $
+  Nothing -> throwInternal $
     "Can't define a custom linearization with symbolic zeros: " ++
     "the SymbolicTangent type is not in scope."
-  Just _ -> throw TypeErr "SymbolicTangent should name a `data` type"
+  Just _ -> throwInternal $ "SymbolicTangent should name a `data` type"
 
 symbolicTangentZero :: EnvReader m => SType n -> m n (SAtom n)
 symbolicTangentZero argTy = return $ toAtom $ SumCon [UnitTy, argTy] 0 UnitVal
diff --git a/src/lib/CheapReduction.hs b/src/lib/CheapReduction.hs
index 8df743f2..41bd2f1d 100644
--- a/src/lib/CheapReduction.hs
+++ b/src/lib/CheapReduction.hs
@@ -29,7 +29,7 @@ import Core
 import Err
 import IRVariants
 import Name
-import PPrint ()
+import PPrint
 import QueryTypePure
 import Types.Core
 import Types.Top
diff --git a/src/lib/CheckType.hs b/src/lib/CheckType.hs
index 9bcbf029..580039a8 100644
--- a/src/lib/CheckType.hs
+++ b/src/lib/CheckType.hs
@@ -22,7 +22,7 @@ import IRVariants
 import MTL1
 import Name
 import Subst
-import PPrint ()
+import PPrint
 import QueryType
 import Types.Core
 import Types.Primitives
@@ -56,7 +56,7 @@ affineUsed name = TyperM $ do
   case lookupNameMapE name affines of
     Just (LiftE n) ->
         if n > 0 then
-          throw TypeErr $ "Affine name " ++ pprint name ++ " used " ++ show (n + 1) ++ " times."
+          throwInternal $ "Affine name " ++ pprint name ++ " used " ++ show (n + 1) ++ " times."
         else
           put $ insertNameMapE name (LiftE $ n + 1) affines
     Nothing -> put $ insertNameMapE name (LiftE 1) affines
@@ -90,7 +90,7 @@ checkTypesEq reqTy ty = alphaEq reqTy ty >>= \case
   False -> {-# SCC typeNormalization #-} do
     alphaEq reqTy ty >>= \case
       True  -> return ()
-      False -> throw TypeErr $ pprint reqTy ++ " != " ++ pprint ty
+      False -> throwInternal $ pprint reqTy ++ " != " ++ pprint ty
 {-# INLINE checkTypesEq #-}
 
 class SinkableE e => CheckableE (r::IR) (e::E) | e -> r where
@@ -407,7 +407,7 @@ instance IRRep r => CheckableE r (Con r) where
     ProdCon xs -> ProdCon <$> mapM checkE xs
     SumCon tys tag payload -> do
       tys' <- mapM checkE tys
-      unless (0 <= tag && tag < length tys') $ throw TypeErr "Invalid SumType tag"
+      unless (0 <= tag && tag < length tys') $ throwInternal "Invalid SumType tag"
       payload' <- payload |: (tys' !! tag)
       return $ SumCon tys' tag payload'
     HeapVal -> return HeapVal
@@ -570,7 +570,7 @@ instance IRRep r => CheckableWithEffects r (MiscOp r) where
       case (destTy', sourceTy) of
         (BaseTy dbt@(Scalar _), BaseTy sbt@(Scalar _)) | sizeOf sbt == sizeOf dbt ->
           return $ BitcastOp destTy' e'
-        _ -> throw TypeErr $ "Invalid bitcast: " ++ pprint sourceTy ++ " -> " ++ pprint destTy
+        _ -> throwInternal $ "Invalid bitcast: " ++ pprint sourceTy ++ " -> " ++ pprint destTy
     UnsafeCoerce t e -> UnsafeCoerce <$> checkE t <*> renameM e
     GarbageVal t -> GarbageVal <$> checkE t
     SumTag x -> do
@@ -616,14 +616,14 @@ instance IRRep r => CheckableE r (VectorOp r) where
       TabTy _ b (BaseTy (Scalar sbt)) <- return $ getType tbl'
       i' <- i |: binderType b
       ty'@(BaseTy (Vector _ sbt')) <- checkE ty
-      unless (sbt == sbt') $ throw TypeErr "Scalar type mismatch"
+      unless (sbt == sbt') $ throwInternal "Scalar type mismatch"
       return $ VectorIdx tbl' i' ty'
     VectorSubref ref i ty -> do
       ref' <- checkE ref
       RefTy _ (TabTy _ b (BaseTy (Scalar sbt))) <- return $ getType ref'
       i' <- i |: binderType b
       ty'@(BaseTy (Vector _ sbt')) <- checkE ty
-      unless (sbt == sbt') $ throw TypeErr "Scalar type mismatch"
+      unless (sbt == sbt') $ throwInternal "Scalar type mismatch"
       return $ VectorSubref ref' i' ty'
 
 checkHof :: IRRep r => EffTy r o -> Hof r i -> TyperM r i o (Hof r o)
@@ -706,7 +706,7 @@ instance IRRep r => CheckableWithEffects r (DAMOp r) where
       checkExtends effs effAnn'
       ixTy' <- checkE ixTy
       (carry', carryTy') <- checkAndGetType carry
-      let badCarry = throw TypeErr $ "Seq carry should be a product of raw references, got: " ++ pprint carryTy'
+      let badCarry = throwInternal $ "Seq carry should be a product of raw references, got: " ++ pprint carryTy'
       case carryTy' of
         TyCon (ProdType refTys) -> forM_ refTys \case RawRefTy _ -> return (); _ -> badCarry
         _ -> badCarry
@@ -773,7 +773,7 @@ checkProject i x = case getType x of
   TyCon (DepPairTy t) | i == 1 -> do
     xFst <- reduceProj 0 x
     checkInstantiation t [xFst]
-  xTy -> throw TypeErr $ "Not a product type:" ++ pprint xTy
+  xTy -> throwInternal $ "Not a product type:" ++ pprint xTy
 
 checkTabApp :: (IRRep r) => Type r o -> Atom r o -> TyperM r i o (Type r o)
 checkTabApp ty i = do
@@ -794,7 +794,7 @@ checkInstantiation abTop xsTop = do
     checkTypesEq (getType x) (binderType b)
     rest <- applySubst (b@>SubstVal x) (Abs bs body)
     go rest xs
-  go _ _ = throw ZipErr "Wrong number of args"
+  go _ _ = throwInternal "Wrong number of args"
 
 checkIntBaseType :: Fallible m => BaseType -> m ()
 checkIntBaseType t = case t of
@@ -809,7 +809,7 @@ checkIntBaseType t = case t of
       Word32Type -> return ()
       Word64Type -> return ()
       _          -> notInt
-    notInt = throw TypeErr $
+    notInt = throwInternal $
       "Expected a fixed-width scalar integer type, but found: " ++ pprint t
 
 checkFloatBaseType :: Fallible m => BaseType -> m ()
@@ -822,13 +822,13 @@ checkFloatBaseType t = case t of
       Float64Type -> return ()
       Float32Type -> return ()
       _           -> notFloat
-    notFloat = throw TypeErr $
+    notFloat = throwInternal $
       "Expected a fixed-width scalar floating-point type, but found: " ++ pprint t
 
 checkValidCast :: (Fallible1 m, IRRep r) => Type r n -> Type r n -> m n ()
 checkValidCast (TyCon (BaseType l)) (TyCon (BaseType r)) = checkValidBaseCast l r
 checkValidCast sourceTy destTy =
-  throw TypeErr $ "Can't cast " ++ pprint sourceTy ++ " to " ++ pprint destTy
+  throwInternal $ "Can't cast " ++ pprint sourceTy ++ " to " ++ pprint destTy
 
 checkValidBaseCast :: Fallible m => BaseType -> BaseType -> m ()
 checkValidBaseCast (PtrType _) (PtrType _) = return ()
@@ -838,13 +838,13 @@ checkValidBaseCast (Scalar _) (Scalar _) = return ()
 checkValidBaseCast sourceTy@(Vector sourceSizes _) destTy@(Vector destSizes _) =
   assertEq sourceSizes destSizes $ "Can't cast " ++ pprint sourceTy ++ " to " ++ pprint destTy
 checkValidBaseCast sourceTy destTy =
-  throw TypeErr $ "Can't cast " ++ pprint sourceTy ++ " to " ++ pprint destTy
+  throwInternal $ "Can't cast " ++ pprint sourceTy ++ " to " ++ pprint destTy
 
 scalarOrVectorLike :: Fallible m => BaseType -> ScalarBaseType -> m BaseType
 scalarOrVectorLike x sbt = case x of
   Scalar _ -> return $ Scalar sbt
   Vector sizes _ -> return $ Vector sizes sbt
-  _ -> throw CompilerErr "only scalar or vector base types should occur here"
+  _ -> throwInternal $ "only scalar or vector base types should occur here"
 
 data ArgumentType = SomeFloatArg | SomeIntArg | SomeUIntArg
 
diff --git a/src/lib/ConcreteSyntax.hs b/src/lib/ConcreteSyntax.hs
index 70bc67b9..6104c4df 100644
--- a/src/lib/ConcreteSyntax.hs
+++ b/src/lib/ConcreteSyntax.hs
@@ -25,6 +25,7 @@ import Data.Void
 import Text.Megaparsec hiding (Label, State)
 import Text.Megaparsec.Char hiding (space, eol)
 
+import Err
 import Lexing
 import Types.Core
 import Types.Source
diff --git a/src/lib/Err.hs b/src/lib/Err.hs
index 51b34eb1..649525f3 100644
--- a/src/lib/Err.hs
+++ b/src/lib/Err.hs
@@ -6,14 +6,15 @@
 
 {-# LANGUAGE UndecidableInstances #-}
 
-module Err (Err (..), ErrType (..), Except (..),
-            Fallible (..), Catchable (..), catchErrExcept,
-            HardFailM (..), runHardFail, throw,
-            catchIOExcept, liftExcept, liftExceptAlt,
-            assertEq, ignoreExcept,
-            pprint, docAsStr, getCurrentCallStack, printCurrentCallStack,
-            ExceptT (..)
-            ) where
+module Err (
+  Err (..), Except (..), ToErr (..), PrintableErr (..),
+  ParseErr (..), SyntaxErr (..), NameErr (..), TypeErr (..), MiscErr (..),
+  Fallible (..), Catchable (..), catchErrExcept,
+  HardFailM (..), runHardFail, throw,
+  catchIOExcept, liftExcept, liftExceptAlt,
+  ignoreExcept, getCurrentCallStack, printCurrentCallStack,
+  ExceptT (..), rootSrcId, SrcId (..), assertEq, throwInternal,
+  InferenceArgDesc, InfVarDesc (..)) where
 
 import Control.Exception hiding (throw)
 import Control.Applicative
@@ -22,40 +23,285 @@ import Control.Monad.Identity
 import Control.Monad.Writer.Strict
 import Control.Monad.State.Strict
 import Control.Monad.Reader
+import Data.Aeson (ToJSON, ToJSONKey)
 import Data.Coerce
+import Data.Hashable
+import Data.List (sort)
 import Data.Foldable (fold)
-import Data.Text.Prettyprint.Doc
+import Data.Store (Store (..))
 import GHC.Stack
+import GHC.Generics
 
 import PPrint
 
--- === core API ===
-
-data Err = Err ErrType String  deriving (Show, Eq)
-
-data ErrType = NoErr
-             | ParseErr
-             | SyntaxErr
-             | TypeErr
-             | KindErr
-             | LinErr
-             | VarDefErr
-             | UnboundVarErr
-             | AmbiguousVarErr
-             | RepeatedVarErr
-             | RepeatedPatVarErr
-             | InvalidPatternErr
-             | CompilerErr
-             | IRVariantErr
-             | NotImplementedErr
-             | DataIOErr
-             | MiscErr
-             | RuntimeErr
-             | ZipErr
-             | EscapedNameErr
-             | ModuleImportErr
-             | SearchFailure -- used as the identity for `Alternative` instances and for MonadFail
-               deriving (Show, Eq)
+-- === source info ===
+
+-- XXX: 0 is reserved for the root The IDs are generated from left to right in
+-- parsing order, so IDs for lexemes are guaranteed to be sorted correctly.
+newtype SrcId = SrcId Int  deriving (Show, Eq, Ord, Generic)
+
+rootSrcId :: SrcId
+rootSrcId = SrcId 0
+
+-- === core errro type ===
+
+data Err =
+   SearchFailure String      -- used as the identity for `Alternative` instances and for MonadFail.
+ | InternalErr String
+ | ParseErr  ParseErr
+ | SyntaxErr SyntaxErr
+ | NameErr   NameErr
+ | TypeErr   TypeErr
+ | RuntimeErr
+ | MiscErr   MiscErr
+   deriving (Show, Eq)
+
+type MsgStr  = String
+type VarStr  = String
+type TypeStr = String
+
+data ParseErr =
+  MiscParseErr MsgStr
+  deriving (Show, Eq)
+
+data SyntaxErr =
+   MiscSyntaxErr MsgStr
+ | TopLevelArrowBinder
+ | CantConstrainAnonBinders
+ | UnexpectedBinder
+ | OnlyUnaryWithoutParens
+ | IllegalPattern
+ | UnexpectedConstraint
+ | ExpectedIdentifier String
+ | UnexpectedEffectForm
+ | UnexpectedMethodDef
+ | BlockWithoutFinalExpr
+ | UnexpectedGivenClause
+ | ArgsShouldHaveParens
+ | BadEqualSign
+ | BadColon
+ | ExpectedAnnBinder
+ | BadField
+ | BadPrefix VarStr
+   deriving (Show, Eq)
+
+data NameErr =
+   MiscNameErr MsgStr
+ | UnboundVarErr VarStr    -- name of var
+ | EscapedNameErr [VarStr] -- names
+ | RepeatedPatVarErr VarStr
+ | RepeatedVarErr VarStr
+ | NotAnOrdinaryVar VarStr
+ | NotADataCon VarStr
+ | NotAClassName VarStr
+ | NotAMethodName VarStr
+ | AmbiguousVarErr VarStr [String]
+ | VarDefErr VarStr
+   deriving (Show, Eq)
+
+data TypeErr =
+   MiscTypeErr MsgStr
+ | CantSynthDict     TypeStr
+ | CantSynthInfVars  TypeStr
+ | NotASynthType     TypeStr
+ | CantUnifySkolem
+ | OccursCheckFailure VarStr TypeStr
+ | UnificationFailure TypeStr TypeStr [VarStr]  -- expected, actual, inference vars
+ | DisallowedEffects  String String  -- allowed, actual
+ | InferEmptyTable
+ | ArityErr        Int Int  -- expected, actual
+ | PatternArityErr Int Int  -- expected, actual
+ | SumTypeCantFail
+ | PatTypeErr String String  -- expected type constructor (from pattern), actual type (from rhs)
+ | EliminationErr String String  -- expected type constructor, actual type
+ | IllFormedCasePattern
+ | NotAMethod VarStr VarStr
+ | DuplicateMethod VarStr
+ | MissingMethod   VarStr
+ | WrongArrowErr String String
+ | AnnotationRequired
+ | NotAUnaryConstraint TypeStr
+ | InterfacesNoImplicitParams
+ | RepeatedOptionalArgs [VarStr]
+ | UnrecognizedOptionalArgs [VarStr] [VarStr]
+ | NoFields TypeStr
+ | TypeMismatch TypeStr TypeStr  -- TODO: should we merege this with UnificationFailure
+ | InferHoleErr
+ | InferDepPairErr
+ | InferEmptyCaseEff
+ | UnexpectedTerm String TypeStr
+ | CantFindField VarStr TypeStr [VarStr]  -- field name, field type, known fields
+ | TupleLengthMismatch Int Int
+ | CantReduceType TypeStr
+ | CantReduceDict
+ | CantReduceDependentArg
+ | AmbiguousInferenceVar VarStr TypeStr InfVarDesc
+ | FFIResultTyErr    TypeStr
+ | FFIArgTyNotScalar TypeStr
+   deriving (Show, Eq)
+
+data MiscErr =
+   MiscMiscErr MsgStr
+ | ModuleImportErr VarStr
+ | CantFindModuleSource VarStr
+   deriving (Show, Eq)
+
+-- name of function, name of arg
+type InferenceArgDesc = (String, String)
+data InfVarDesc =
+   ImplicitArgInfVar InferenceArgDesc
+ | AnnotationInfVar String -- name of binder
+ | TypeInstantiationInfVar String -- name of type
+ | MiscInfVar
+   deriving (Show, Generic, Eq, Ord)
+
+-- === ToErr class ===
+
+class ToErr a where
+  toErr :: a -> Err
+
+instance ToErr Err where toErr = id
+instance ToErr ParseErr  where toErr = ParseErr
+instance ToErr SyntaxErr where toErr = SyntaxErr
+instance ToErr NameErr   where toErr = NameErr
+instance ToErr TypeErr   where toErr = TypeErr
+instance ToErr MiscErr   where toErr = MiscErr
+
+-- === Error messages ===
+
+class PrintableErr a where
+  printErr :: a -> String
+
+instance PrintableErr Err where
+  printErr = \case
+    SearchFailure s -> "Internal search failure: " ++ s
+    InternalErr s -> "Internal compiler error: " ++ s ++ "\n" ++
+      "Please report this at github.com/google-research/dex-lang/issues\n"
+    ParseErr   e -> "Parse error: "  ++ printErr e
+    SyntaxErr  e -> "Syntax error: " ++ printErr e
+    NameErr    e -> "Name error: "   ++ printErr e
+    TypeErr    e -> "Type error: "   ++ printErr e
+    MiscErr    e -> "Error: "        ++ printErr e
+    RuntimeErr   -> "Runtime error"
+
+instance PrintableErr ParseErr where
+  printErr = \case
+    MiscParseErr s -> s
+
+instance PrintableErr SyntaxErr where
+  printErr = \case
+    MiscSyntaxErr s -> s
+    TopLevelArrowBinder ->
+      "Arrow binder syntax <- not permitted at the top level, because the binding would have unbounded scope."
+    CantConstrainAnonBinders -> "can't constrain anonymous binders"
+    UnexpectedBinder -> "binder must be an identifier or `_`"
+    OnlyUnaryWithoutParens ->"only unary constructors can form patterns without parens"
+    IllegalPattern -> "illegal pattern"
+    UnexpectedConstraint -> "unexpected constraint"
+    ExpectedIdentifier ctx -> "expected " ++ ctx ++ " to be an identifier"
+    UnexpectedEffectForm ->
+      "unexpected effect form; expected one of `Read h`, `Accum h`, `State h`, `Except`, `IO`, "
+       ++ "or the name of a user-defined effect."
+    UnexpectedMethodDef -> "unexpected method definition. Expected `def` or `x = ...`."
+    BlockWithoutFinalExpr -> "block must end in expression"
+    UnexpectedGivenClause -> "unexpected `given` clause"
+    ArgsShouldHaveParens -> "argument types should be in parentheses"
+    BadEqualSign -> "equal sign must be used as a separator for labels or binders, not a standalone operator"
+    BadColon ->
+      "colon separates binders from their type annotations, is not a standalone operator.\n"
+      ++ " If you are trying to write a dependent type, use parens: (i:Fin 4) => (..i)"
+    ExpectedAnnBinder -> "expected an annotated binder"
+    BadField -> "field must be a name or an integer"
+    BadPrefix name -> "prefix (" ++ name ++ ") not legal as a bare expression"
+
+instance PrintableErr NameErr where
+  printErr = \case
+    MiscNameErr s -> s
+    UnboundVarErr v     -> "variable not in scope: " ++ v
+    EscapedNameErr vs   -> "leaked local variables: " ++ unwords vs
+    RepeatedPatVarErr v -> "variable already defined within pattern: " ++ v
+    RepeatedVarErr    v -> "variable already defined : " ++ v
+    NotAnOrdinaryVar v -> "not an ordinary variable: " ++ v
+    NotADataCon      v -> "not a data constructor: "   ++ v
+    NotAClassName    v -> "not a class name: "         ++ v
+    NotAMethodName   v -> "not a method name: "        ++ v
+    -- we sort the lines to make the result a bit more deterministic for quine tests
+    AmbiguousVarErr v defs ->
+      "ambiguous occurrence: " ++ v ++ " is defined:\n"
+      ++ unlines (sort defs)
+    -- TODO: we see this message a lot. We should improve it by including more information.
+    -- Ideally we'd provide a link to where the original error happened."
+    VarDefErr v -> "error in (earlier) definition of variable: " ++ v
+
+instance PrintableErr TypeErr where
+  printErr = \case
+    MiscTypeErr s -> s
+    FFIResultTyErr t    -> "FFI result type should be scalar or pair. Got: " ++ t
+    FFIArgTyNotScalar t -> "FFI function arguments should be scalar. Got: " ++ t
+    CantSynthDict t     -> "can't synthesize a class dictionary for: " ++ t
+    CantSynthInfVars t  -> "can't synthesize a class dictionary for a type with inference vars: " ++ t
+    NotASynthType t     -> "can't synthesize terms of type: " ++ t
+    CantUnifySkolem     -> "can't unify with skolem vars"
+    OccursCheckFailure v t -> "occurs check failure: " ++ v ++ " occurs in " ++ t
+    DisallowedEffects r1 r2 -> "\nAllowed:   " ++ pprint r1 ++
+                               "\nRequested: " ++ pprint r2
+    UnificationFailure t1 t2 vs -> "\nExpected: " ++ t1
+                                ++ "\nActual: " ++ t2 ++ case vs of
+                                                          [] -> ""
+                                                          _  -> "\n(Solving for: " ++ unwords vs ++ ")"
+    InferEmptyTable       -> "can't infer type of empty table"
+    ArityErr n1 n2 -> "wrong number of positional arguments provided. Expected " ++ show n1 ++ " but got " ++ show n2
+    PatternArityErr n1 n2 -> "unexpected number of pattern binders. Expected "   ++ show n1 ++ " but got " ++ show n2
+    SumTypeCantFail               -> "sum type constructor in can't-fail pattern"
+    PatTypeErr patTy rhsTy        -> "pattern is for a " ++ patTy ++ "but we're matching against a " ++ rhsTy
+    EliminationErr expected ty    -> "expected a " ++ expected ++ ". Got a: " ++ ty
+    IllFormedCasePattern          -> "case patterns must start with a data constructor or variant pattern"
+    NotAMethod method className   -> "unexpected method: " ++ method ++ " is not a method of " ++ className
+    DuplicateMethod method        -> "duplicate method: " ++ method
+    MissingMethod   method        -> "missing method: "   ++ method
+    WrongArrowErr expected actual -> "wrong arrow. Expected " ++ expected ++ " got " ++ actual
+    AnnotationRequired            -> "type annotation or constraint required"
+    NotAUnaryConstraint ty        -> "constraint should be a unary function. Got: " ++ ty
+    InterfacesNoImplicitParams    -> "interfaces can't have implicit parameters"
+    RepeatedOptionalArgs vs       -> "repeated names offered:" ++ unwords vs
+    UnrecognizedOptionalArgs vs accepted -> "unrecognized named arguments: " ++ unwords vs
+                                       ++ ". Should be one of: " ++ pprint accepted
+    NoFields ty -> "can't get fields for type " ++ pprint ty
+    TypeMismatch expected actual -> "\nExpected: " ++ expected ++
+                                    "\nActual:   " ++ actual
+    InferHoleErr -> "can't infer value of hole"
+    InferDepPairErr -> "can't infer the type of a dependent pair; please annotate its type"
+    InferEmptyCaseEff -> "can't infer empty case expressions"
+    UnexpectedTerm term ty -> "unexpected " ++ term ++ ". Expected: " ++ ty
+    CantFindField field fieldTy knownFields ->
+      "can't resolve field " ++ field ++ " of type " ++ fieldTy ++
+      "\nKnown fields are: " ++ unwords knownFields
+    TupleLengthMismatch req actual -> do
+        "tuple length mismatch. Expected: " ++ show req ++ " but got " ++ show actual
+    CantReduceType  ty -> "Can't reduce type expression: " ++ ty
+    CantReduceDict -> "Can't reduce dict"
+    CantReduceDependentArg ->
+      "dependent functions can only be applied to fully evaluated expressions. " ++
+      "Bind the argument to a name before you apply the function."
+    AmbiguousInferenceVar infVar ty desc -> case desc of
+       AnnotationInfVar v ->
+         "couldn't infer type of unannotated binder " <> v
+       ImplicitArgInfVar (f, argName) ->
+         "couldn't infer implicit argument `" <> argName <> "` of " <> f
+       TypeInstantiationInfVar t ->
+         "couldn't infer instantiation of type " <> t
+       MiscInfVar ->
+         "ambiguous type variable: " ++ infVar ++ ": " ++ ty
+
+instance PrintableErr MiscErr where
+  printErr = \case
+    MiscMiscErr s -> s
+    ModuleImportErr v -> "couldn't import " ++ v
+    CantFindModuleSource v ->
+      "couldn't find a source file for module " ++ v ++
+      "\nHint: Consider extending --lib-path"
+
+-- === monads and helpers ===
 
 class MonadFail m => Fallible m where
   throwErr :: Err -> m a
@@ -68,7 +314,7 @@ catchErrExcept m = catchErr (Success <$> m) (\e -> return $ Failure e)
 
 catchSearchFailure :: Catchable m => m a -> m (Maybe a)
 catchSearchFailure m = (Just <$> m) `catchErr` \case
-  Err SearchFailure _ -> return Nothing
+  SearchFailure _ -> return Nothing
   err -> throwErr err
 
 instance Fallible IO where
@@ -104,7 +350,7 @@ instance Monad m => Monad (ExceptT m) where
   {-# INLINE (>>=) #-}
 
 instance Monad m => MonadFail (ExceptT m) where
-  fail s = ExceptT $ return $ Failure $ Err SearchFailure s
+  fail s = ExceptT $ return $ Failure $ SearchFailure s
   {-# INLINE fail #-}
 
 instance Monad m => Fallible (ExceptT m) where
@@ -112,7 +358,7 @@ instance Monad m => Fallible (ExceptT m) where
   {-# INLINE throwErr #-}
 
 instance Monad m => Alternative (ExceptT m) where
-  empty = throw SearchFailure ""
+  empty = throwErr $ SearchFailure ""
   {-# INLINE empty #-}
   m1 <|> m2 = do
     catchSearchFailure m1 >>= \case
@@ -164,7 +410,7 @@ instance Monad Except where
   {-# INLINE (>>=) #-}
 
 instance Alternative Except where
-  empty = throw SearchFailure ""
+  empty = throwErr $ SearchFailure ""
   {-# INLINE empty #-}
   m1 <|> m2 = do
     catchSearchFailure m1 >>= \case
@@ -218,8 +464,8 @@ instance Fallible HardFailM where
 
 -- === convenience layer ===
 
-throw :: Fallible m => ErrType -> String -> m a
-throw errTy s = throwErr $ Err errTy s
+throw :: (ToErr e, Fallible m) => e -> m a
+throw e = throwErr $ toErr e
 {-# INLINE throw #-}
 
 getCurrentCallStack :: () -> Maybe [String]
@@ -240,12 +486,12 @@ printCurrentCallStack (Just frames) = fold frames
 catchIOExcept :: MonadIO m => IO a -> m (Except a)
 catchIOExcept m = liftIO $ (liftM Success m) `catches`
   [ Handler \(e::Err)           -> return $ Failure e
-  , Handler \(e::IOError)        -> return $ Failure $ Err DataIOErr   $ show e
+  , Handler \(e::IOError)        -> return $ Failure $ MiscErr $ MiscMiscErr $ show e
   -- Propagate asynchronous exceptions like ThreadKilled; they are
   -- part of normal operation (of the live evaluation modes), not
   -- compiler bugs.
   , Handler \(e::AsyncException) -> liftIO $ throwIO e
-  , Handler \(e::SomeException)  -> return $ Failure $ Err CompilerErr $ show e
+  , Handler \(e::SomeException)  -> return $ Failure $ InternalErr $ show e
   ]
 
 liftExcept :: Fallible m => Except a -> m a
@@ -266,10 +512,12 @@ ignoreExcept (Success x) = x
 
 assertEq :: (HasCallStack, Fallible m, Show a, Pretty a, Eq a) => a -> a -> String -> m ()
 assertEq x y s = if x == y then return ()
-                           else throw CompilerErr msg
+                           else throwInternal msg
   where msg = "assertion failure (" ++ s ++ "):\n"
-              ++ pprint x ++ " != " ++ pprint y ++ "\n\n"
-              ++ prettyCallStack callStack ++ "\n"
+              ++ pprint x ++ " != " ++ pprint y
+
+throwInternal :: (HasCallStack, Fallible m) => String -> m a
+throwInternal s = throwErr $ InternalErr $ s ++ "\n" ++ prettyCallStack callStack ++ "\n"
 
 instance (Monoid w, Fallible m) => Fallible (WriterT w m) where
   throwErr errs = lift $ throwErr errs
@@ -290,49 +538,11 @@ instance Fallible Except where
   {-# INLINE throwErr #-}
 
 instance MonadFail Except where
-  fail s = Failure $ Err SearchFailure s
+  fail s = Failure $ SearchFailure s
   {-# INLINE fail #-}
 
 instance Exception Err
 
-instance Pretty Err where
-  pretty (Err e s) = pretty e <> pretty s
-
-instance Pretty a => Pretty (Except a) where
-  pretty (Success x) = "Success:" <+> pretty x
-  pretty (Failure e) = "Failure:" <+> pretty e
-
-instance Pretty ErrType where
-  pretty e = case e of
-    -- NoErr tags a chunk of output that was promoted into the Err ADT
-    -- by appending Results.
-    NoErr             -> ""
-    ParseErr          -> "Parse error:"
-    SyntaxErr         -> "Syntax error: "
-    TypeErr           -> "Type error:"
-    KindErr           -> "Kind error:"
-    LinErr            -> "Linearity error: "
-    IRVariantErr      -> "Internal IR validation error: "
-    VarDefErr         -> "Error in (earlier) definition of variable: "
-    UnboundVarErr     -> "Error: variable not in scope: "
-    AmbiguousVarErr   -> "Error: ambiguous variable: "
-    RepeatedVarErr    -> "Error: variable already defined: "
-    RepeatedPatVarErr -> "Error: variable already defined within pattern: "
-    InvalidPatternErr -> "Error: not a valid pattern: "
-    NotImplementedErr ->
-      "Not implemented:" <> line <>
-      "Please report this at github.com/google-research/dex-lang/issues\n" <> line
-    CompilerErr       ->
-      "Compiler bug!" <> line <>
-      "Please report this at github.com/google-research/dex-lang/issues\n" <> line
-    DataIOErr         -> "IO error: "
-    MiscErr           -> "Error:"
-    RuntimeErr        -> "Runtime error"
-    ZipErr            -> "Zipping error"
-    EscapedNameErr    -> "Leaked local variables:"
-    ModuleImportErr   -> "Module import error: "
-    SearchFailure     -> "Search error (internal error)"
-
 instance Fallible m => Fallible (ReaderT r m) where
   throwErr errs = lift $ throwErr errs
   {-# INLINE throwErr #-}
@@ -348,3 +558,12 @@ instance Fallible m => Fallible (StateT s m) where
 instance Catchable m => Catchable (StateT s m) where
   StateT f `catchErr` handler = StateT \s ->
     f s `catchErr` \e -> runStateT (handler e) s
+
+instance Pretty Err where
+  pretty e = pretty $ printErr e
+
+instance ToJSON SrcId
+deriving instance ToJSONKey SrcId
+
+instance Hashable InfVarDesc
+instance Store InfVarDesc
diff --git a/src/lib/Export.hs b/src/lib/Export.hs
index 1108507f..85459572 100644
--- a/src/lib/Export.hs
+++ b/src/lib/Export.hs
@@ -21,6 +21,7 @@ import Foreign.Ptr
 import Builder
 import Core
 import Err
+import PPrint
 import IRVariants
 import Name
 import QueryType
@@ -47,11 +48,11 @@ prepareFunctionForExport :: (Mut n, Topper m)
 prepareFunctionForExport cc f = do
   naryPi <- case getType f of
     TyCon (Pi piTy) -> return piTy
-    _ -> throw TypeErr "Only first-order functions can be exported"
+    _ -> throw $ MiscMiscErr "Only first-order functions can be exported"
   sig <- liftExportSigM $ corePiToExportSig cc naryPi
   closedSig <- case hoistToTop sig of
     HoistFailure _ ->
-      throw TypeErr $ "Types of exported functions have to be closed terms. Got: " ++ pprint naryPi
+      throw $ MiscMiscErr $ "Types of exported functions have to be closed terms. Got: " ++ pprint naryPi
     HoistSuccess s -> return s
   f' <- liftBuilder $ buildCoreLam naryPi \xs -> naryApp (sink f) (toAtom <$> xs)
   fSimp <- simplifyTopFunction $ coreLamToTopLam f'
@@ -67,7 +68,7 @@ prepareSLamForExport cc f@(TopLam _ naryPi _) = do
   sig <- liftExportSigM $ simpPiToExportSig cc naryPi
   closedSig <- case hoistToTop sig of
     HoistFailure _ ->
-      throw TypeErr $ "Types of exported functions have to be closed terms. Got: " ++ pprint naryPi
+      throw $ MiscMiscErr $ "Types of exported functions have to be closed terms. Got: " ++ pprint naryPi
     HoistSuccess s -> return s
   fImp <- compileTopLevelFun cc f
   nativeFun <- toCFunction "userFunc" fImp >>= emitObjFile >>= loadObject
@@ -104,7 +105,7 @@ corePiToExportSig :: CallingConvention
 corePiToExportSig cc (CorePiType _ expls tbs (EffTy effs resultTy)) = do
     case effs of
       Pure -> return ()
-      _    -> throw TypeErr "Only pure functions can be exported"
+      _    -> throw $ MiscMiscErr "Only pure functions can be exported"
     goArgs cc Empty [] (zipAttrs expls tbs) resultTy
 
 simpPiToExportSig :: CallingConvention
@@ -112,7 +113,7 @@ simpPiToExportSig :: CallingConvention
 simpPiToExportSig cc (PiType bs (EffTy effs resultTy)) = do
   case effs of
     Pure -> return ()
-    _    -> throw TypeErr "Only pure functions can be exported"
+    _    -> throw $ MiscMiscErr "Only pure functions can be exported"
   bs' <- return $ fmapNest (\b -> WithAttrB Explicit b) bs
   goArgs cc Empty [] bs' resultTy
 
@@ -163,7 +164,7 @@ toExportType ty = case ty of
     Nothing  -> unsupported
     Just ety -> return ety
   _ -> unsupported
-  where unsupported = throw TypeErr $ "Unsupported type of argument in exported function: " ++ pprint ty
+  where unsupported = throw $ MiscMiscErr $ "Unsupported type of argument in exported function: " ++ pprint ty
 {-# INLINE toExportType #-}
 
 parseTabTy :: IRRep r => Type r i -> ExportSigM r i o (Maybe (ExportType o))
diff --git a/src/lib/Generalize.hs b/src/lib/Generalize.hs
index 7ace599c..fc120af2 100644
--- a/src/lib/Generalize.hs
+++ b/src/lib/Generalize.hs
@@ -11,6 +11,7 @@ import Data.Maybe (fromJust)
 
 import Core
 import Err
+import PPrint
 import Types.Core
 import Inference
 import IRVariants
diff --git a/src/lib/Imp.hs b/src/lib/Imp.hs
index 07fada48..18f3f700 100644
--- a/src/lib/Imp.hs
+++ b/src/lib/Imp.hs
@@ -37,6 +37,7 @@ import Err
 import IRVariants
 import MTL1
 import Name
+import PPrint
 import Subst
 import QueryType
 import Types.Core
diff --git a/src/lib/ImpToLLVM.hs b/src/lib/ImpToLLVM.hs
index f333c1f0..e5736b35 100644
--- a/src/lib/ImpToLLVM.hs
+++ b/src/lib/ImpToLLVM.hs
@@ -45,7 +45,6 @@ import qualified Data.Set as S
 import CUDA (getCudaArchitecture)
 
 import Core
-import Err
 import Imp
 import LLVM.CUDA (LLVMKernel (..), compileCUDAKernel, ptxDataLayout, ptxTargetTriple)
 import Subst
diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs
index bea45b65..67227f3d 100644
--- a/src/lib/Inference.hs
+++ b/src/lib/Inference.hs
@@ -22,7 +22,6 @@ import Data.Foldable (toList, asum)
 import Data.Functor ((<&>))
 import Data.List (sortOn)
 import Data.Maybe (fromJust, fromMaybe, catMaybes)
-import Data.Text.Prettyprint.Doc (Pretty (..))
 import Data.Word
 import qualified Data.HashMap.Strict as HM
 import qualified Data.Map.Strict as M
@@ -38,6 +37,7 @@ import MonadUtil
 import MTL1
 import Name
 import Subst
+import PPrint
 import QueryType
 import Types.Core
 import Types.Imp
@@ -214,17 +214,6 @@ applySolverSubst subst e = do
   return $ fmapNames env (lookupSolverSubst subst) e
 {-# INLINE applySolverSubst #-}
 
-formatAmbiguousVarErr :: CAtomName n -> CType n' -> InfVarDesc -> String
-formatAmbiguousVarErr infVar ty = \case
-  AnnotationInfVar v ->
-    "Couldn't infer type of unannotated binder " <> v
-  ImplicitArgInfVar (f, argName) ->
-    "Couldn't infer implicit argument `" <> argName <> "` of " <> f
-  TypeInstantiationInfVar t ->
-    "Couldn't infer instantiation of type " <> t
-  MiscInfVar ->
-    "Ambiguous type variable: " ++ pprint infVar ++ ": " ++ pprint ty
-
 withFreshBinderInf :: NameHint -> Explicitness -> CType o -> InfererCPSB CBinder i o a
 withFreshBinderInf hint expl ty cont =
   withFreshBinder hint ty \b -> do
@@ -290,7 +279,7 @@ withFreshUnificationVar desc k cont = do
     ans <- toAtomVar v >>= cont
     soln <- (M.lookup v <$> fromSolverSubst <$> getDiffState) >>= \case
       Just soln ->  return soln
-      Nothing -> throw TypeErr $ formatAmbiguousVarErr v k desc
+      Nothing -> throw $ AmbiguousInferenceVar (pprint v) (pprint k) desc
     return (ans, soln)
 {-# INLINE withFreshUnificationVar #-}
 
@@ -362,6 +351,18 @@ emitTypeInfo sid ty = do
   InfererM $ liftSubstReaderT $ lift11 $ lift1 $ lift do
     modify \(TypeInfo m) -> TypeInfo $ M.insert sid ty m
 
+withReducibleEmissions
+  :: (HasNamesE e, SubstE AtomSubstVal e, ToErr err)
+  => err
+  -> (forall o' . (Emits o', DExt o o') => InfererM i o' (e o'))
+  -> InfererM i o (e o)
+withReducibleEmissions msg cont = do
+  withDecls <- buildScoped cont
+  reduceWithDecls withDecls >>= \case
+    Just t -> return t
+    _ -> throw msg
+{-# INLINE withReducibleEmissions #-}
+
 -- === actual inference pass ===
 
 data RequiredTy (n::S) =
@@ -420,13 +421,13 @@ topDownExplicit :: forall i o. Emits o => CType o -> UExpr i -> InfererM i o (CA
 topDownExplicit reqTy exprWithSrc@(WithSrcE _ expr) = case expr of
   ULam lamExpr -> case reqTy of
     TyCon (Pi piTy) -> toAtom <$> Lam <$> checkULam lamExpr piTy
-    _       -> throw TypeErr $ "Unexpected lambda. Expected: " ++ pprint reqTy
+    _       -> throw $ UnexpectedTerm "lambda" (pprint reqTy)
   UFor dir uFor -> case reqTy of
     TyCon (TabPi tabPiTy) -> do
       lam@(UnaryLamExpr b' _) <- checkUForExpr uFor tabPiTy
       ixTy <- asIxType $ binderType b'
       emitHof $ For dir ixTy lam
-    _ -> throw TypeErr $ "Unexpected `for` expression. Expected: " ++ pprint reqTy
+    _ -> throw $ UnexpectedTerm "`for` expression" (pprint reqTy)
   UApp f posArgs namedArgs -> do
     f' <- bottomUpExplicit f
     checkOrInferApp f' posArgs namedArgs (Check reqTy)
@@ -436,7 +437,7 @@ topDownExplicit reqTy exprWithSrc@(WithSrcE _ expr) = case expr of
       rhsTy <- instantiate ty [lhs']
       rhs' <- topDown rhsTy rhs
       return $ toAtom $ DepPair lhs' rhs' ty
-    _ -> throw TypeErr $ "Unexpected dependent pair. Expected: " ++ pprint reqTy
+    _ -> throw $ UnexpectedTerm "dependent pair" (pprint reqTy)
   UCase scrut alts -> do
     scrut' <- bottomUp scrut
     let scrutTy = getType scrut'
@@ -446,15 +447,15 @@ topDownExplicit reqTy exprWithSrc@(WithSrcE _ expr) = case expr of
   UTabCon xs -> do
     case reqTy of
       TyCon (TabPi tabPiTy) -> checkTabCon tabPiTy xs
-      _ -> throw TypeErr $ "Unexpected table constructor. Expected: " ++ pprint reqTy
+      _ -> throw $ UnexpectedTerm "table constructor" (pprint reqTy)
   UNatLit x -> fromNatLit x reqTy
   UIntLit x -> fromIntLit x reqTy
   UPrim UTuple xs -> case reqTy of
     TyKind -> toAtom . ProdType <$> mapM checkUType xs
     TyCon (ProdType reqTys) -> do
-      when (length reqTys /= length xs) $ throw TypeErr "Tuple length mismatch"
+      when (length reqTys /= length xs) $ throw $ TupleLengthMismatch (length reqTys) (length xs)
       toAtom <$> ProdCon <$> forM (zip reqTys xs) \(reqTy', x) -> topDown reqTy' x
-    _ -> throw TypeErr $ "Unexpected tuple. Expected: " ++ pprint reqTy
+    _ -> throw $ UnexpectedTerm "tuple" (pprint reqTy)
   UFieldAccess _ _ -> infer
   UVar _           -> infer
   UTypeAnn _ _     -> infer
@@ -465,7 +466,7 @@ topDownExplicit reqTy exprWithSrc@(WithSrcE _ expr) = case expr of
   UPi _            -> infer
   UTabPi _         -> infer
   UDepPairTy _     -> infer
-  UHole -> throw TypeErr "Can't infer value of hole"
+  UHole -> throw InferHoleErr
   where
     infer :: InfererM i o (CAtom o)
     infer = do
@@ -495,9 +496,7 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
           method' <- toAtomVar method
           resultTy <- partialAppType (getType method') (params ++ [x'])
           return $ SigmaPartialApp resultTy (toAtom method') (params ++ [x'])
-      Nothing -> throw TypeErr $
-        "Can't resolve field " ++ pprint field ++ " of type " ++ pprint ty ++
-        "\nKnown fields are: " ++ pprint (M.keys fields)
+      Nothing -> throw $ CantFindField (pprint field) (pprint ty) (map pprint $ M.keys fields)
   ULam lamExpr -> SigmaAtom Nothing <$> toAtom <$> inferULam lamExpr
   UFor dir uFor -> do
     lam@(UnaryLamExpr b' _) <- inferUForExpr uFor
@@ -525,8 +524,7 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
     withUBinder b \(WithAttrB _ b') -> do
       rhs' <- checkUType rhs
       return $ SigmaAtom Nothing $ toAtom $ DepPairTy $ DepPairType expl b' rhs'
-  UDepPair _ _ -> throw TypeErr $
-    "Can't infer the type of a dependent pair; please annotate its type"
+  UDepPair _ _ -> throw InferDepPairErr
   UCase scrut (alt:alts) -> do
     scrut' <- bottomUp scrut
     let scrutTy = getType scrut'
@@ -536,7 +534,7 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
     resultTy <- liftHoistExcept $ hoist b ty
     alts' <- mapM (checkCaseAlt (Check resultTy) scrutTy) alts
     SigmaAtom Nothing <$> buildSortedCase scrut' (alt':alts') resultTy
-  UCase _ [] -> throw TypeErr "Can't infer empty case expressions"
+  UCase _ [] -> throw InferEmptyCaseEff
   UDo block -> withBlockDecls block \result -> bottomUpExplicit result
   UTabCon xs -> liftM (SigmaAtom Nothing) $ inferTabCon xs
   UTypeAnn val ty -> do
@@ -548,7 +546,7 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
   UPrim UMonoLiteral [WithSrcE _ l] -> case l of
     UIntLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Int32Lit $ fromIntegral x
     UNatLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Word32Lit $ fromIntegral x
-    _ -> throw MiscErr "argument to %monoLit must be a literal"
+    _ -> throwInternal "argument to %monoLit must be a literal"
   UPrim UExplicitApply (f:xs) -> do
     f' <- bottomUpExplicit f
     xs' <- mapM bottomUp xs
@@ -567,13 +565,12 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
   UNatLit l -> liftM (SigmaAtom Nothing) $ fromNatLit l NatTy
   UIntLit l -> liftM (SigmaAtom Nothing) $ fromIntLit l (BaseTy $ Scalar Int32Type)
   UFloatLit x -> return $ SigmaAtom Nothing $ Con $ Lit  $ Float32Lit $ realToFrac x
-  UHole -> throw TypeErr "Can't infer value of hole"
+  UHole -> throw InferHoleErr
 
 expectEq :: (PrettyE e, AlphaEqE e) => e o -> e o -> InfererM i o ()
 expectEq reqTy actualTy = alphaEq reqTy actualTy >>= \case
   True -> return ()
-  False -> throw TypeErr $ "Expected: " ++ pprint reqTy ++
-                         "\nActual:   " ++ pprint actualTy
+  False -> throw $ TypeMismatch (pprint reqTy) (pprint actualTy)
 {-# INLINE expectEq #-}
 
 fromIntLit :: Emits o => Int -> CType o -> InfererM i o (CAtom o)
@@ -692,7 +689,7 @@ data FieldDef (n::S) =
 
 getFieldDefs :: CType n -> InfererM i n (M.Map FieldName' (FieldDef n))
 getFieldDefs ty = case ty of
-  StuckTy _ _ -> noFields ""
+  StuckTy _ _ -> noFields
   TyCon con -> case con of
     NewtypeTyCon (UserADTType _ tyName params) -> do
       TyConBinding ~(Just tyDef) (DotMethods dotMethods) <- lookupEnv tyName
@@ -703,9 +700,9 @@ getFieldDefs ty = case ty of
           let methodFields = M.toList dotMethods <&> \(field, f) ->
                 (FieldName field, FieldDotMethod f params)
           return $ M.fromList $ concat projFields ++ methodFields
-        ADTCons _ -> noFields ""
+        ADTCons _ -> noFields
     RefType _ valTy -> case valTy of
-      RefTy _ _ -> noFields ""
+      RefTy _ _ -> noFields
       _ -> do
         valFields <- getFieldDefs valTy
         return $ M.filter isProj valFields
@@ -713,10 +710,9 @@ getFieldDefs ty = case ty of
                 FieldProj _ -> True
                 _ -> False
     ProdType ts -> return $ M.fromList $ enumerate ts <&> \(i, _) -> (FieldNum i, FieldProj i)
-    TabPi _ -> noFields "\nArray indexing uses [] now."
-    _ -> noFields ""
-  where
-    noFields s = throw TypeErr $ "Can't get fields for type " ++ pprint ty ++ s
+    TabPi _ -> noFields
+    _ -> noFields
+  where noFields = throw $ NoFields $ pprint ty
 
 projectField :: Emits o => Int -> CAtom o -> InfererM i o (CAtom o)
 projectField i x = case getType x of
@@ -773,7 +769,7 @@ checkOrInferApp f' posArgs namedArgs reqTy = do
         args <- inferMixedArgs fDesc expls bsConstrained (posArgs, namedArgs)
         applySigmaAtom f args
       ImplicitApp -> error "should already have handled this case"
-    ty -> throw TypeErr $ "Expected a function type. Got: " ++ pprint ty
+    ty -> throw $ EliminationErr "function type" (pprint ty)
  where
   fDesc :: SourceName
   fDesc = getSourceName f'
@@ -891,9 +887,7 @@ checkExplicitArity :: [Explicitness] -> [a] -> InfererM i o ()
 checkExplicitArity expls args = do
   let arity = length [() | Explicit <- expls]
   let numArgs = length args
-  when (numArgs /= arity) do
-    throw TypeErr $ "Wrong number of positional arguments provided. Expected " ++
-      pprint arity ++ " but got " ++ pprint numArgs
+  when (numArgs /= arity) $ throw $ ArityErr arity numArgs
 
 type MixedArgs arg = ([arg], [(SourceName, arg)])  -- positional args, named args
 data Constraint (n::S) =
@@ -1022,12 +1016,10 @@ checkNamedArgValidity expls offeredNames = do
         Inferred v _ -> v
   let acceptedNames = catMaybes $ map explToMaybeName expls
   let duplicates = repeated offeredNames
-  when (not $ null duplicates) do
-    throw TypeErr $ "Repeated names offered" ++ pprint duplicates
+  when (not $ null duplicates) $ throw $ RepeatedOptionalArgs $ map pprint duplicates
   let unrecognizedNames = filter (not . (`elem` acceptedNames)) offeredNames
   when (not $ null unrecognizedNames) do
-    throw TypeErr $ "Unrecognized named arguments: " ++ pprint unrecognizedNames
-      ++ "\nShould be one of: " ++ pprint acceptedNames
+    throw $ UnrecognizedOptionalArgs (map pprint unrecognizedNames) (map pprint acceptedNames)
 
 inferPrimArg :: Emits o => UExpr i -> InfererM i o (CAtom o)
 inferPrimArg x = do
@@ -1035,7 +1027,7 @@ inferPrimArg x = do
   case getType xBlock of
     TyKind -> reduceExpr xBlock >>= \case
       Just reduced -> return reduced
-      _ -> throw CompilerErr "Type args to primops must be reducible"
+      _ -> throwInternal "Type args to primops must be reducible"
     _ -> emit xBlock
 
 matchPrimApp :: Emits o => PrimName -> [CAtom o] -> InfererM i o (CAtom o)
@@ -1077,7 +1069,7 @@ matchPrimApp = \case
    combiner' <- lam2 combiner
    f' <- lam2 f
    emitHof $ RunWriter Nothing (BaseMonoid idVal combiner') f'
- p -> \case xs -> throw TypeErr $ "Bad primitive application: " ++ show (p, xs)
+ p -> \case xs -> throwInternal $ "Bad primitive application: " ++ show (p, xs)
  where
    lam2 :: Fallible m => CAtom n -> m (LamExpr CoreIR n)
    lam2 x = do
@@ -1127,14 +1119,11 @@ inferNaryTabAppArgs tabTy (arg:rest) = case tabTy of
     resultTy' <- applySubst (b @> SubstVal arg') resultTy
     rest' <- inferNaryTabAppArgs resultTy' rest
     return $ arg':rest'
-  _ -> throw TypeErr $ "Expected a table type but got: " ++ pprint tabTy
+  _ -> throw $ EliminationErr "table type" (pprint tabTy)
 
 checkSigmaDependent :: UExpr i -> PartialType o -> InfererM i o (CAtom o)
-checkSigmaDependent e ty = withReducibleEmissions depFunErrMsg $ topDownPartial (sink ty) e
-  where
-    depFunErrMsg =
-      "Dependent functions can only be applied to fully evaluated expressions. " ++
-      "Bind the argument to a name before you apply the function."
+checkSigmaDependent e ty = withReducibleEmissions CantReduceDependentArg $
+  topDownPartial (sink ty) e
 
 -- === sorting case alternatives ===
 
@@ -1285,7 +1274,7 @@ inferClassDef className methodNames paramBs methodTys = do
     PairB paramBs'' superclassBs <- partitionBinders (zipAttrs roleExpls paramBs') $
       \b@(WithAttrB (_, expl) b') -> case expl of
         Explicit -> return $ LeftB b
-        Inferred _ Unify -> throw TypeErr "Interfaces can't have implicit parameters"
+        Inferred _ Unify -> throw InterfacesNoImplicitParams
         Inferred _ (Synth _) -> return $ RightB b'
     let (roleExpls', paramBs''') = unzipAttrs paramBs''
     builtinName <- case className of
@@ -1354,16 +1343,15 @@ inferAnn ann cs = case ann of
     WithSrcE _ (UVar ~(InternalName _ _ v)):_ -> do
       renameM v >>= getUVarType >>= \case
         TyCon (Pi (CorePiType ExplicitApp [Explicit] (UnaryNest (_:>ty)) _)) -> return ty
-        ty -> throw TypeErr $ "Constraint should be a unary function. Got: " ++ pprint ty
-    _ -> throw TypeErr "Type annotation or constraint required"
+        ty -> throw $ NotAUnaryConstraint $ pprint ty
+    _ -> throw AnnotationRequired
 
 checkULamPartial :: PartialPiType o -> ULamExpr i -> InfererM i o (CoreLamExpr o)
 checkULamPartial partialPiTy lamExpr = do
   PartialPiType piAppExpl expls piBs piEffs piReqTy <- return partialPiTy
   ULamExpr lamBs lamAppExpl lamEffs lamResultTy body <- return lamExpr
   checkExplicitArity expls (nestToList (const ()) lamBs)
-  when (piAppExpl /= lamAppExpl) $ throw TypeErr $ "Wrong arrow. Expected "
-     ++ pprint piAppExpl ++ " got " ++ pprint lamAppExpl
+  when (piAppExpl /= lamAppExpl) $ throw $ WrongArrowErr (pprint piAppExpl) (pprint lamAppExpl)
   checkLamBinders expls piBs lamBs \lamBs' -> do
     PairE piEffs' piReqTy' <- applyRename (piBs @@> (atomVarName <$> bindersVars lamBs')) (PairE piEffs piReqTy)
     resultTy <- case (lamResultTy, piReqTy') of
@@ -1470,10 +1458,8 @@ checkInstanceBody className params methods = do
   ListE methodTys'' <- applySubst (scBs'@@>(SubstVal<$>superclassDicts)) methodTys'
   methodsChecked <- mapM (checkMethodDef className methodTys'') methods
   let (idxs, methods') = unzip $ sortOn fst $ methodsChecked
-  forM_ (repeated idxs) \i ->
-    throw TypeErr $ "Duplicate method: " ++ pprint (methodNames!!i)
-  forM_ ([0..(length methodTys'' - 1)] `listDiff` idxs) \i ->
-    throw TypeErr $ "Missing method: " ++ pprint (methodNames!!i)
+  forM_ (repeated idxs) \i -> throw $ DuplicateMethod $ pprint (methodNames!!i)
+  forM_ ([0..(length methodTys''-1)] `listDiff` idxs) \i -> throw $ MissingMethod $ pprint (methodNames!!i)
   return $ InstanceBody superclassDicts methods'
 
 superclassDictTys :: Nest CBinder o o' -> InfererM i o [CType o]
@@ -1488,7 +1474,7 @@ checkMethodDef className methodTys (WithSrcE _ m) = do
   MethodBinding className' i <- renameM v >>= lookupEnv
   when (className /= className') do
     ClassBinding classDef <- lookupEnv className
-    throw TypeErr $ pprint sourceName ++ " is not a method of " ++ pprint (getSourceName classDef)
+    throw $ NotAMethod (pprint sourceName) (pprint $ getSourceName classDef)
   (i,) <$> toAtom <$> Lam <$> checkULam rhs (methodTys !! i)
 
 checkUEffRow :: UEffectRow i -> InfererM i o (EffectRow CoreIR o)
@@ -1525,7 +1511,7 @@ getCaseAltIndex (WithSrcB _ pat) = case pat of
   UPatCon ~(InternalName _ _ conName) _ -> do
     (_, con) <- renameM conName >>= lookupDataCon
     return con
-  _ -> throw TypeErr $ "Case patterns must start with a data constructor or variant pattern"
+  _ -> throw IllFormedCasePattern
 
 checkCasePat
   :: Emits o
@@ -1539,15 +1525,13 @@ checkCasePat (WithSrcB _ pat) scrutineeTy cont = case pat of
     params <- inferParams scrutineeTy dataDefName
     ADTCons cons <- instantiateTyConDef tyConDef params
     DataConDef _ _ repTy idxs <- return $ cons !! con
-    when (length idxs /= nestLength ps) $ throw TypeErr $
-      "Unexpected number of pattern binders. Expected " ++ show (length idxs)
-                                             ++ " got " ++ show (nestLength ps)
+    when (length idxs /= nestLength ps) $ throw $ PatternArityErr (length idxs) (nestLength ps)
     withFreshBinderInf noHint Explicit repTy \b -> Abs b <$> do
       buildBlock do
         args <- forM idxs \projs -> do
           emitToVar =<< applyProjectionsReduced (init projs) (sink $ toAtom $ binderVar b)
         bindLetPats ps args $ cont
-  _ -> throw TypeErr $ "Case patterns must start with a data constructor or variant pattern"
+  _ -> throw IllFormedCasePattern
 
 inferParams :: Emits o => CType o -> TyConName o -> InfererM i o (TyConParams o)
 inferParams ty dataDefName = do
@@ -1582,13 +1566,13 @@ bindLetPat (WithSrcB _ pat) v cont = case pat of
     let n = nestLength ps
     case getType v of
       TyCon (ProdType ts) | length ts == n -> return ()
-      ty -> throw TypeErr $ "Expected a product type but got: " ++ pprint ty
+      ty -> throw $ PatTypeErr "product type" (pprint ty)
     xs <- forM (iota n) \i -> proj i (toAtom v) >>= emitInline
     bindLetPats ps xs cont
   UPatDepPair (PairB p1 p2) -> do
     case getType v of
       TyCon (DepPairTy _) -> return ()
-      ty -> throw TypeErr $ "Expected a dependent pair, but got: " ++ pprint ty
+      ty -> throw $ PatTypeErr "dependent pair" (pprint ty)
     -- XXX: we're careful here to reduce the projection because of the dependent
     -- types. We do the same in the `UPatCon` case.
     x1 <- reduceProj 0 (toAtom v) >>= emitInline
@@ -1601,18 +1585,17 @@ bindLetPat (WithSrcB _ pat) v cont = case pat of
     TyConDef _ _ _ cons <- lookupTyCon dataDefName
     case cons of
       ADTCons [DataConDef _ _ _ idxss] -> do
-        when (length idxss /= nestLength ps) $ throw TypeErr $
-          "Unexpected number of pattern binders. Expected " ++ show (length idxss)
-                                                 ++ " got " ++ show (nestLength ps)
+        when (length idxss /= nestLength ps) $
+          throw $ PatternArityErr (length idxss) (nestLength ps)
         void $ inferParams (getType $ toAtom v) dataDefName
         xs <- forM idxss \idxs -> applyProjectionsReduced idxs (toAtom v) >>= emitInline
         bindLetPats ps xs cont
-      _ -> throw TypeErr $ "sum type constructor in can't-fail pattern"
+      _ -> throw SumTypeCantFail
   UPatTable ps -> do
     let n = fromIntegral (nestLength ps) :: Word32
     case getType v of
       TyCon (TabPi (TabPiType _ (_:>FinConst n') _)) | n == n' -> return ()
-      ty -> throw TypeErr $ "Expected a Fin " ++ show n ++ " table type but got: " ++ pprint ty
+      ty -> throw $ PatTypeErr ("Fin " ++ show n ++ " table") (pprint ty)
     xs <- forM [0 .. n - 1] \i -> do
       emitToVar =<< mkTabApp (toAtom v) (toAtom $ NewtypeCon (FinCon (NatVal n)) (NatVal $ fromIntegral i))
     bindLetPats ps xs cont
@@ -1628,14 +1611,14 @@ checkUType t = do
 checkUParam :: Kind CoreIR o -> UType i -> InfererM i o (CAtom o)
 checkUParam k uty =
   withReducibleEmissions msg $ withAllowedEffects Pure $ topDownExplicit (sink k) uty
-  where msg = "Can't reduce type expression: " ++ pprint uty
+  where msg = CantReduceType $ pprint uty
 
 inferTabCon :: forall i o. Emits o => [UExpr i] -> InfererM i o (CAtom o)
 inferTabCon xs = do
   let n = fromIntegral (length xs) :: Word32
   let finTy = FinConst n
   elemTy <- case xs of
-    []  -> throw TypeErr "Can't infer type of empty table"
+    []  -> throw InferEmptyTable
     x:_ -> getType <$> bottomUp x
   ixTy <- asIxType finTy
   let tabTy = ixTy ==> elemTy
@@ -1697,8 +1680,7 @@ applyConstraint = \case
     -- any inference variables in r2's explicit effects because we don't know
     -- how they line up with r1's. So this is just about figuring out r2's tail.
     r2 <- zonk r2'
-    let msg = "Allowed effects:   " ++ pprint r1 ++
-            "\nRequested effects: " ++ pprint r2
+    let msg = DisallowedEffects (pprint r1) (pprint r2)
     case checkExtends r1 r2 of
       Success () -> return ()
       Failure _  -> searchFailureAsTypeErr msg do
@@ -1713,18 +1695,14 @@ constrainEq :: ToAtom e CoreIR => e o -> e o -> SolverM i o ()
 constrainEq t1 t2 = do
   t1' <- zonk $ toAtom t1
   t2' <- zonk $ toAtom t2
-  msg <- liftEnvReaderM $ do
+  msg <- liftEnvReaderM do
     ab <- renameForPrinting $ PairE t1' t2'
     return $ canonicalizeForPrinting ab \(Abs infVars (PairE t1Pretty t2Pretty)) ->
-              "Expected: " ++ pprint t1Pretty
-         ++ "\n  Actual: " ++ pprint t2Pretty
-         ++ (case infVars of
-               Empty -> ""
-               _ -> "\n(Solving for: " ++ pprint (nestToList pprint infVars) ++ ")")
+      UnificationFailure (pprint t1Pretty) (pprint t2Pretty) (nestToList pprint infVars)
   void $ searchFailureAsTypeErr msg $ unify t1' t2'
 
-searchFailureAsTypeErr :: String -> SolverM i n a -> SolverM i n a
-searchFailureAsTypeErr msg cont = cont <|> throw TypeErr msg
+searchFailureAsTypeErr :: ToErr e => e -> SolverM i n a -> SolverM i n a
+searchFailureAsTypeErr msg cont = cont <|> throw msg
 {-# INLINE searchFailureAsTypeErr #-}
 
 class AlphaEqE e => Unifiable (e::E) where
@@ -1964,13 +1942,13 @@ extendSolution :: CAtomVar n -> CAtom n -> SolverM i n ()
 extendSolution (AtomVar v _) t =
   isUnificationName v >>= \case
     True -> do
-      when (v `isFreeIn` t) $ throw TypeErr $ "Occurs check failure: " ++ pprint (v, t)
+      when (v `isFreeIn` t) $ throw $ OccursCheckFailure (pprint v) (pprint t)
       -- When we unify under a pi binder we replace its occurrences with a
       -- skolem variable. We don't want to unify with terms containing these
       -- variables because that would mean inferring dependence, which is a can
       -- of worms.
       forM_ (freeAtomVarsList t) \fv ->
-        whenM (isSkolemName fv) $ throw TypeErr $ "Can't unify with skolem vars"
+        whenM (isSkolemName fv) $ throw CantUnifySkolem
       addConstraint v t
     False -> empty
 
@@ -2090,11 +2068,11 @@ emitInstanceDef instanceDef@(InstanceDef className _ _ _ _) = do
 trySynthTerm :: CType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n)
 trySynthTerm ty reqMethodAccess = do
   hasInferenceVars ty >>= \case
-    True -> throw TypeErr $ "Can't synthesize a dictionary for a type with inference vars: " ++ pprint ty
+    True -> throw $ CantSynthInfVars $ pprint ty
     False -> withVoidSubst do
       synthTy <- liftExcept $ typeAsSynthType ty
       synthTerm synthTy reqMethodAccess
-        <|> throw TypeErr ("Couldn't synthesize a class dictionary for: " ++ pprint ty)
+        <|> (throw $ CantSynthDict $ pprint ty)
 {-# SCC trySynthTerm #-}
 
 hasInferenceVars :: (EnvReader m, HoistableE e) => e n -> m n Bool
@@ -2139,7 +2117,7 @@ typeAsSynthType = \case
   TyCon (DictTy dictTy) -> return $ SynthDictType dictTy
   TyCon (Pi (CorePiType ImplicitApp expls bs (EffTy Pure (TyCon (DictTy d))))) ->
     return $ SynthPiType (expls, Abs bs d)
-  ty -> Failure $ Err TypeErr $ "Can't synthesize terms of type: " ++ pprint ty
+  ty -> Failure $ toErr $ NotASynthType $ pprint ty
 {-# SCC typeAsSynthType #-}
 
 getSuperclassClosure :: EnvReader m => Givens n -> [SynthAtom n] -> m n (Givens n)
@@ -2254,7 +2232,7 @@ addInstanceSynthCandidate className maybeBuiltin instanceName = do
 
 instantiateSynthArgs :: DictType n -> SynthPiType n -> InfererM i n [CAtom n]
 instantiateSynthArgs target (expls, synthPiTy) = do
-  liftM fromListE $ withReducibleEmissions "dict args" do
+  liftM fromListE $ withReducibleEmissions CantReduceDict do
     bsConstrained <- buildConstraints (sink synthPiTy) \_ resultTy -> do
       return [TypeConstraint (TyCon $ DictTy $ sink target) (TyCon $ DictTy resultTy)]
     ListE <$> inferMixedArgs "dict" expls bsConstrained emptyMixedArgs
@@ -2263,10 +2241,9 @@ emptyMixedArgs :: MixedArgs (CAtom n)
 emptyMixedArgs = ([], [])
 
 typeErrAsSearchFailure :: InfererM i n a -> InfererM i n a
-typeErrAsSearchFailure cont = cont `catchErr` \err@(Err errTy _) -> do
-  case errTy of
-    TypeErr -> empty
-    _ -> throwErr err
+typeErrAsSearchFailure cont = cont `catchErr` \case
+  TypeErr _ -> empty
+  e -> throwErr e
 
 synthDictForData :: forall i n. DictType n -> InfererM i n (SynthAtom n)
 synthDictForData dictTy@(DataDictType ty) = case ty of
@@ -2352,7 +2329,7 @@ checkFFIFunTypeM _ = error "expected at least one argument"
 
 checkScalar :: (IRRep r, Fallible m) => Type r n -> m BaseType
 checkScalar (BaseTy ty) = return ty
-checkScalar ty = throw TypeErr $ pprint ty
+checkScalar ty = throw $ FFIArgTyNotScalar $ pprint ty
 
 checkScalarOrPairType :: (IRRep r, Fallible m) => Type r n -> m [BaseType]
 checkScalarOrPairType (PairTy a b) = do
@@ -2360,7 +2337,7 @@ checkScalarOrPairType (PairTy a b) = do
   tys2 <- checkScalarOrPairType b
   return $ tys1 ++ tys2
 checkScalarOrPairType (BaseTy ty) = return [ty]
-checkScalarOrPairType ty = throw TypeErr $ pprint ty
+checkScalarOrPairType ty = throw $ FFIResultTyErr $ pprint ty
 
 -- === instances ===
 
diff --git a/src/lib/Lexing.hs b/src/lib/Lexing.hs
index 4d3b6dc8..111027ff 100644
--- a/src/lib/Lexing.hs
+++ b/src/lib/Lexing.hs
@@ -24,6 +24,7 @@ import qualified Text.Megaparsec.Char.Lexer as L
 import Text.Megaparsec.Debug
 
 import Err
+import PPrint
 import Types.Primitives
 import Types.Source
 import Util (toSnocList)
@@ -43,7 +44,7 @@ type Parser = StateT ParseCtx (Parsec Void Text)
 
 parseit :: Text -> Parser a -> Except a
 parseit s p = case parse (fst <$> runStateT p initParseCtx) "" s of
-  Left e  -> throw ParseErr $ errorBundlePretty e
+  Left e  -> throw $ MiscParseErr $ errorBundlePretty e
   Right x -> return x
 
 mustParseit :: Text -> Parser a -> a
diff --git a/src/lib/Name.hs b/src/lib/Name.hs
index fd23def5..4f025384 100644
--- a/src/lib/Name.hs
+++ b/src/lib/Name.hs
@@ -2757,12 +2757,7 @@ pprintCanonicalized e = canonicalizeForPrinting e \e' -> pprint e'
 
 liftHoistExcept :: Fallible m => HoistExcept a -> m a
 liftHoistExcept (HoistSuccess x) = return x
-liftHoistExcept (HoistFailure vs) = throw EscapedNameErr (pprint vs)
-
-liftHoistExcept' :: Fallible m => String -> HoistExcept a -> m a
-liftHoistExcept' _ (HoistSuccess x) = return x
-liftHoistExcept' msg (HoistFailure vs) =
-  throw EscapedNameErr $ (pprint vs) ++ "\n" ++ msg
+liftHoistExcept (HoistFailure vs) = throw $ EscapedNameErr $ map pprint vs
 
 ignoreHoistFailure :: HasCallStack => HoistExcept a -> a
 ignoreHoistFailure (HoistSuccess x) = x
@@ -2864,7 +2859,7 @@ partitionBinders bs assignBinder = go bs where
         RightB b2 -> withSubscopeDistinct bs2
           case exchangeBs (PairB b2 bs1) of
             HoistSuccess (PairB bs1' b2') -> return $ PairB bs1' (Nest b2' bs2)
-            HoistFailure vs -> throw EscapedNameErr $ (pprint vs)
+            HoistFailure vs -> throw $ EscapedNameErr $ map pprint vs
 
 -- NameBinder has no free vars, so there's no risk associated with hoisting.
 -- The scope is completely distinct, so their exchange doesn't create any accidental
diff --git a/src/lib/QueryType.hs b/src/lib/QueryType.hs
index a6e3b4b5..acbff02c 100644
--- a/src/lib/QueryType.hs
+++ b/src/lib/QueryType.hs
@@ -8,6 +8,7 @@ module QueryType (module QueryType, module QueryTypePure, toAtomVar) where
 
 import Control.Category ((>>>))
 import Control.Monad
+import Control.Applicative
 import Data.List (elemIndex)
 import Data.Maybe (fromJust)
 import Data.Functor ((<&>))
@@ -23,14 +24,14 @@ import Err
 import Name hiding (withFreshM)
 import Subst
 import Util
-import PPrint ()
+import PPrint
 import QueryTypePure
 import CheapReduction
 
 sourceNameType :: (EnvReader m, Fallible1 m) => SourceName -> m n (Type CoreIR n)
 sourceNameType v = do
   lookupSourceMap v >>= \case
-    Nothing -> throw UnboundVarErr $ pprint v
+    Nothing -> throw $ UnboundVarErr $ pprint v
     Just uvar -> getUVarType uvar
 
 -- === Exposed helpers for querying types and effects ===
@@ -347,35 +348,29 @@ liftIFunType (IFunType _ argTys resultTys) = liftEnvReaderM $ go argTys where
 
 isData :: EnvReader m => Type CoreIR n -> m n Bool
 isData ty = do
-  result <- liftEnvReaderT $ withSubstReaderT $ checkDataLike ty
+  result <- liftEnvReaderT $ withSubstReaderT $ go ty
   case result of
-    Success () -> return True
-    Failure _  -> return False
-
-checkDataLike :: Type CoreIR i -> SubstReaderT Name (EnvReaderT Except) i o ()
-checkDataLike ty = case ty of
-  StuckTy _ _ -> notData
-  TyCon con -> case con of
-    TabPi (TabPiType _ b eltTy) -> do
-      renameBinders b \_ ->
-        checkDataLike eltTy
-    DepPairTy (DepPairType _ b@(_:>l) r) -> do
-      recur l
-      renameBinders b \_ -> checkDataLike r
-    NewtypeTyCon nt -> do
-      (_, ty') <- unwrapNewtypeType =<< renameM nt
-      dropSubst $ recur ty'
-    BaseType _       -> return ()
-    ProdType as      -> mapM_ recur as
-    SumType  cs      -> mapM_ recur cs
-    RefType _ _      -> return ()
-    HeapType         -> return ()
-    TypeKind -> notData
-    DictTy _ -> notData
-    Pi _     -> notData
+    Just () -> return True
+    Nothing -> return False
   where
-    recur = checkDataLike
-    notData = throw TypeErr $ pprint ty
+    go :: Type CoreIR i -> SubstReaderT Name (EnvReaderT Maybe) i o ()
+    go = \case
+      StuckTy _ _ -> notData
+      TyCon con -> case con of
+        TabPi (TabPiType _ b eltTy) -> renameBinders b \_ -> go eltTy
+        DepPairTy (DepPairType _ b@(_:>l) r) -> go l >> renameBinders b \_ -> go r
+        NewtypeTyCon nt -> do
+          (_, ty') <- unwrapNewtypeType =<< renameM nt
+          dropSubst $ go ty'
+        BaseType _  -> return ()
+        ProdType as -> mapM_ go as
+        SumType  cs -> mapM_ go cs
+        RefType _ _ -> return ()
+        HeapType    -> return ()
+        TypeKind -> notData
+        DictTy _ -> notData
+        Pi _     -> notData
+      where notData = empty
 
 checkExtends :: (Fallible m, IRRep r) => EffectRow r n -> EffectRow r n -> m ()
 checkExtends allowed (EffectRow effs effTail) = do
@@ -384,6 +379,6 @@ checkExtends allowed (EffectRow effs effTail) = do
     EffectRowTail _ -> assertEq allowedEffTail effTail ""
     NoTail -> return ()
   forM_ (eSetToList effs) \eff -> unless (eff `eSetMember` allowedEffs) $
-    throw CompilerErr $ "Unexpected effect: " ++ pprint eff ++
-                      "\nAllowed: " ++ pprint allowed
+    throwInternal $ "Unexpected effect: " ++ pprint eff ++
+                       "\nAllowed: " ++ pprint allowed
 {-# INLINE checkExtends #-}
diff --git a/src/lib/RenderHtml.hs b/src/lib/RenderHtml.hs
index 3cbc25c8..e4015c6a 100644
--- a/src/lib/RenderHtml.hs
+++ b/src/lib/RenderHtml.hs
@@ -30,7 +30,7 @@ import GHC.Generics
 
 import Err
 import Paths_dex (getDataFileName)
-import PPrint ()
+import PPrint
 import Types.Source
 import Util (unsnoc, foldJusts)
 
diff --git a/src/lib/Runtime.hs b/src/lib/Runtime.hs
index 20730e33..10201909 100644
--- a/src/lib/Runtime.hs
+++ b/src/lib/Runtime.hs
@@ -72,7 +72,7 @@ checkedCallFunPtr :: FD -> Ptr () -> Ptr () -> DexExecutable -> IO ()
 checkedCallFunPtr fd argsPtr resultPtr fPtr = do
   let (CInt fd') = fdFD fd
   exitCode <- callFunPtr fPtr fd' argsPtr resultPtr
-  unless (exitCode == 0) $ throw RuntimeErr ""
+  unless (exitCode == 0) $ throw RuntimeErr
 
 withPipeToLogger :: PassLogger -> (FD -> IO a) -> IO a
 withPipeToLogger logger writeAction = do
diff --git a/src/lib/RuntimePrint.hs b/src/lib/RuntimePrint.hs
index 15fa1c86..dd12d67a 100644
--- a/src/lib/RuntimePrint.hs
+++ b/src/lib/RuntimePrint.hs
@@ -16,6 +16,7 @@ import IRVariants
 import MTL1
 import Name
 import CheapReduction
+import PPrint
 import Types.Core
 import Types.Source
 import Types.Primitives
diff --git a/src/lib/Simplify.hs b/src/lib/Simplify.hs
index 789ccb59..f44aa109 100644
--- a/src/lib/Simplify.hs
+++ b/src/lib/Simplify.hs
@@ -14,7 +14,6 @@ import Control.Category ((>>>))
 import Control.Monad
 import Control.Monad.Reader
 import Data.Maybe
-import Data.Text.Prettyprint.Doc (Pretty (..), hardline)
 
 import Builder
 import CheapReduction
@@ -26,6 +25,7 @@ import IRVariants
 import Linearize
 import Name
 import Subst
+import PPrint
 import QueryType
 import RuntimePrint
 import Transpose
diff --git a/src/lib/SourceIdTraversal.hs b/src/lib/SourceIdTraversal.hs
index 19ca2f8c..7e243620 100644
--- a/src/lib/SourceIdTraversal.hs
+++ b/src/lib/SourceIdTraversal.hs
@@ -11,6 +11,7 @@ import Data.Functor ((<&>))
 
 import Types.Source
 import Types.Primitives
+import Err
 
 getGroupTree :: SourceBlock' -> GroupTree
 getGroupTree b = mkGroupTree False rootSrcId $ runTreeM $ visit b
diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs
index c6b68d82..1fcaa73d 100644
--- a/src/lib/SourceRename.hs
+++ b/src/lib/SourceRename.hs
@@ -10,7 +10,6 @@ module SourceRename ( renameSourceNamesTopUDecl, uDeclErrSourceMap
                     , renameSourceNamesUExpr ) where
 
 import Prelude hiding (id, (.))
-import Data.List (sort)
 import Control.Category
 import Control.Monad.Except hiding (Except)
 import qualified Data.Set        as S
@@ -19,7 +18,7 @@ import qualified Data.Map.Strict as M
 import Err
 import Name
 import Core (EnvReader (..), withEnv, lookupSourceMapPure)
-import PPrint ()
+import PPrint
 import IRVariants
 import Types.Source
 import Types.Primitives
@@ -107,45 +106,40 @@ lookupSourceName :: Renamer m => SourceName -> m n (UVar n)
 lookupSourceName v = do
   sm <- askSourceMap
   case lookupSourceMapPure sm v of
-    [] -> throw UnboundVarErr $ pprint v
+    [] -> throw $ UnboundVarErr $ pprint v
     LocalVar v' : _ -> return v'
     [ModuleVar _ maybeV] -> case maybeV of
       Just v' -> return v'
-      Nothing -> throw VarDefErr $ pprint v
-    vs -> throw AmbiguousVarErr $ ambiguousVarErrMsg v vs
-
-ambiguousVarErrMsg :: SourceName -> [SourceNameDef n] -> String
-ambiguousVarErrMsg v defs =
-  -- we sort the lines to make the result a bit more deterministic for quine tests
-  pprint v ++ " is defined:\n" ++ unlines (sort $ map defsPretty defs)
-  where
-    defsPretty :: SourceNameDef n -> String
-    defsPretty (ModuleVar mname _) = case mname of
-      Main -> "in this file"
-      Prelude -> "in the prelude"
-      OrdinaryModule mname' -> "in " ++ pprint mname'
-    defsPretty (LocalVar _) =
-      error "shouldn't be possible because module vars can't shadow local ones"
+      Nothing -> throw $ VarDefErr $ pprint v
+    vs -> throw $ AmbiguousVarErr (pprint v) (map wherePretty vs)
+    where
+      wherePretty :: SourceNameDef n -> String
+      wherePretty (ModuleVar mname _) = case mname of
+        Main -> "in this file"
+        Prelude -> "in the prelude"
+        OrdinaryModule mname' -> "in " ++ pprint mname'
+      wherePretty (LocalVar _) =
+        error "shouldn't be possible because module vars can't shadow local ones"
 
 instance SourceRenamableE (SourceNameOr (Name (AtomNameC CoreIR))) where
   sourceRenameE (SourceName pos sourceName) = do
     lookupSourceName sourceName >>= \case
       UAtomVar v -> return $ InternalName pos sourceName v
-      _ -> throw TypeErr $ "Not an ordinary variable: " ++ pprint sourceName
+      _ -> throw $ NotAnOrdinaryVar $ pprint sourceName
   sourceRenameE _ = error "Shouldn't be source-renaming internal names"
 
 instance SourceRenamableE (SourceNameOr (Name DataConNameC)) where
   sourceRenameE (SourceName pos sourceName) = do
     lookupSourceName sourceName >>= \case
       UDataConVar v -> return $ InternalName pos sourceName v
-      _ -> throw TypeErr $ "Not a data constructor: " ++ pprint sourceName
+      _ -> throw $ NotADataCon $ pprint sourceName
   sourceRenameE _ = error "Shouldn't be source-renaming internal names"
 
 instance SourceRenamableE (SourceNameOr (Name ClassNameC)) where
   sourceRenameE (SourceName pos sourceName) = do
     lookupSourceName sourceName >>= \case
       UClassVar v -> return $ InternalName pos sourceName v
-      _ -> throw TypeErr $ "Not a class name: " ++ pprint sourceName
+      _ -> throw $ NotAClassName $ pprint sourceName
   sourceRenameE _ = error "Shouldn't be source-renaming internal names"
 
 instance SourceRenamableE (SourceNameOr (Name c)) => SourceRenamableE (SourceOrInternalName c) where
@@ -310,8 +304,7 @@ sourceRenameUBinder' asUVar ubinder cont = case ubinder of
     SourceMap sm <- askSourceMap
     mayShadow <- askMayShadow
     let shadows = M.member b sm
-    when (not mayShadow && shadows) $
-      throw RepeatedVarErr $ pprint b
+    when (not mayShadow && shadows) $ throw (RepeatedVarErr $ pprint b)
     withFreshM (getNameHint b) \freshName -> do
       Distinct <- getDistinct
       extendSourceMap b (asUVar $ binderName freshName) $
@@ -367,7 +360,7 @@ instance SourceRenamableE UMethodDef' where
   sourceRenameE (UMethodDef ~(SourceName pos v) expr) = do
     lookupSourceName v >>= \case
       UMethodVar v' -> UMethodDef (InternalName pos v v') <$> sourceRenameE expr
-      _ -> throw TypeErr $ "not a method name: " ++ pprint v
+      _ -> throw $ NotAMethodName $ pprint v
 
 instance SourceRenamableB b => SourceRenamableB (Nest b) where
   sourceRenameB (Nest b bs) cont =
@@ -394,7 +387,7 @@ instance SourceRenamablePat (UBinder' (AtomNameC CoreIR)) where
   sourceRenamePat sibs ubinder cont = do
     newSibs <- case ubinder of
       UBindSource b -> do
-        when (S.member b sibs) $ throw RepeatedPatVarErr $ pprint b
+        when (S.member b sibs) $ throw $ RepeatedPatVarErr $ pprint b
         return $ S.singleton b
       UIgnore -> return mempty
       UBind _ _ -> error "Shouldn't be source-renaming internal names"
diff --git a/src/lib/TopLevel.hs b/src/lib/TopLevel.hs
index 69dc417d..47b132c3 100644
--- a/src/lib/TopLevel.hs
+++ b/src/lib/TopLevel.hs
@@ -70,6 +70,7 @@ import Serialize (takePtrSnapshot, restorePtrSnapshot)
 import Simplify
 import SourceRename
 import SourceIdTraversal
+import PPrint
 import Types.Core
 import Types.Imp
 import Types.Primitives
@@ -262,7 +263,7 @@ evalSourceBlock' mname block = case sbContents block of
   DeclareForeign fname (WithSrc _ dexName) cTy -> do
     ty <- evalUType =<< parseExpr cTy
     asFFIFunType ty >>= \case
-      Nothing -> throw TypeErr
+      Nothing -> throw $ MiscMiscErr
         "FFI functions must be n-ary first order functions with the IO effect"
       Just (impFunTy, naryPiTy) -> do
         -- TODO: query linking stuff and check the function is actually available
@@ -274,15 +275,15 @@ evalSourceBlock' mname block = case sbContents block of
   DeclareCustomLinearization fname zeros g -> do
     expr <- parseExpr g
     lookupSourceMap (withoutSrc fname) >>= \case
-      Nothing -> throw UnboundVarErr $ pprint fname
+      Nothing -> throw $ UnboundVarErr $ pprint fname
       Just (UAtomVar fname') -> do
         lookupCustomRules fname' >>= \case
           Nothing -> return ()
-          Just _  -> throw TypeErr
+          Just _  -> throw $ MiscMiscErr
             $ pprint fname ++ " already has a custom linearization"
         lookupAtomName fname' >>= \case
           NoinlineFun _ _ -> return ()
-          _ -> throw TypeErr "Custom linearizations only apply to @noinline functions"
+          _ -> throw $ MiscMiscErr "Custom linearizations only apply to @noinline functions"
         -- We do some special casing to avoid instantiating polymorphic functions.
         impl <- case expr of
           WithSrcE _ (UVar _) ->
@@ -295,14 +296,13 @@ evalSourceBlock' mname block = case sbContents block of
         liftEnvReaderT (impl `checkTypeIs` linFunTy) >>= \case
           Failure _ -> do
             let implTy = getType impl
-            throw TypeErr $ unlines
+            throw $ MiscMiscErr $ unlines
               [ "Expected the custom linearization to have type:" , "" , pprint linFunTy , ""
               , "but it has type:" , "" , pprint implTy]
           Success () -> return ()
         updateTopEnv $ AddCustomRule fname' $ CustomLinearize nimplicit nexplicit zeros impl
-      Just _ -> throw TypeErr
-        $ "Custom linearization can only be defined for functions"
-  UnParseable _ s -> throw ParseErr s
+      Just _ -> throw $ MiscMiscErr $ "Custom linearization can only be defined for functions"
+  UnParseable _ s -> throw $ MiscParseErr s
   Misc m -> case m of
     GetNameType v -> do
       ty <- sourceNameType (withoutSrc v)
@@ -327,11 +327,11 @@ runEnvQuery query = do
     DumpSubst -> logTop $ TextOut $ pprint $ env
     InternalNameInfo name ->
       case lookupSubstFragRaw (fromRecSubst $ envDefs $ topEnv env) name of
-        Nothing      -> throw UnboundVarErr $ pprint name
+        Nothing      -> throw $ UnboundVarErr $ pprint name
         Just binding -> logTop $ TextOut $ pprint binding
     SourceNameInfo name -> do
       lookupSourceMap name >>= \case
-        Nothing -> throw UnboundVarErr $ pprint name
+        Nothing -> throw $ UnboundVarErr $ pprint name
         Just uvar -> do
           logTop $ TextOut $ pprint uvar
           info <- case uvar of
@@ -400,7 +400,7 @@ evalPartiallyParsedUModuleCached md@(UModulePartialParse name deps source) = do
       directDeps <- forM deps \dep -> do
         lookupLoadedModule dep >>= \case
           Just depVal -> return depVal
-          Nothing -> throw CompilerErr $ pprint dep ++ " isn't loaded"
+          Nothing -> throwInternal $ pprint dep ++ " isn't loaded"
       let req = (fHash source, directDeps)
       case M.lookup name cache of
         Just (cachedReq, result) | cachedReq == req -> return result
@@ -434,7 +434,7 @@ evalUModule (UModule name _ blocks) = do
 importModule :: (Mut n, TopBuilder m, Fallible1 m) => ModuleSourceName -> m n ()
 importModule name = do
   lookupLoadedModule name >>= \case
-    Nothing -> throw ModuleImportErr $ "Couldn't import " ++ pprint name
+    Nothing -> throw $ ModuleImportErr $ pprint name
     Just name' -> do
       Module _ _ transImports' _ _ <- lookupModule name'
       let importStatus = ImportStatus (S.singleton name')
@@ -693,13 +693,7 @@ loadModuleSource config moduleName = do
       fsPaths <- liftIO $ traverse resolveBuiltinPath $ libPaths config
       liftIO (findFile fsPaths fname) >>= \case
         Just fpath -> return fpath
-        Nothing    -> throw ModuleImportErr $ unlines
-          [ "Couldn't find a source file for module " ++
-            (case moduleName of
-               OrdinaryModule n -> pprint n; Prelude -> "prelude"; Main -> error "")
-          , "Hint: Consider extending --lib-path?"
-          ]
-
+        Nothing    -> throw $ CantFindModuleSource $ pprint moduleName
     resolveBuiltinPath = \case
       LibBuiltinPath   -> liftIO $ getDataFileName "lib"
       LibDirectory dir -> return dir
@@ -838,14 +832,14 @@ getLinearizationType zeros = \case
         Just tty -> case zeros of
           InstantiateZeros -> return tty
           SymbolicZeros    -> symbolicTangentTy tty
-        Nothing  -> throw TypeErr $ "No tangent type for: " ++ pprint t
+        Nothing  -> throw $ MiscMiscErr $ "No tangent type for: " ++ pprint t
       resultTanTy <- maybeTangentType resultTy' >>= \case
         Just rtt -> return rtt
-        Nothing  -> throw TypeErr $ "No tangent type for: " ++ pprint resultTy'
+        Nothing  -> throw $ MiscMiscErr $ "No tangent type for: " ++ pprint resultTy'
       let tanFunTy = toType $ Pi $ nonDepPiType argTanTys Pure resultTanTy
       let fullTy = CorePiType ExplicitApp expls bs' $ EffTy Pure (PairTy resultTy' tanFunTy)
       return (numIs, numEs, toType $ Pi fullTy)
-  _ -> throw TypeErr $ "Can't define a custom linearization for implicit or impure functions"
+  _ -> throw $ MiscMiscErr $ "Can't define a custom linearization for implicit or impure functions"
   where
     getNumImplicits :: Fallible m => [Explicitness] -> m (Int, Int)
     getNumImplicits = \case
@@ -856,4 +850,4 @@ getLinearizationType zeros = \case
           Inferred _ _ -> return (ni + 1, ne)
           Explicit -> case ni of
             0 -> return (0, ne + 1)
-            _ -> throw TypeErr "All implicit args must precede implicit args"
+            _ -> throw $ MiscMiscErr "All implicit args must precede implicit args"
diff --git a/src/lib/Transpose.hs b/src/lib/Transpose.hs
index e35305bc..3e361d0d 100644
--- a/src/lib/Transpose.hs
+++ b/src/lib/Transpose.hs
@@ -13,10 +13,10 @@ import GHC.Stack
 
 import Builder
 import Core
-import Err
 import Imp
 import IRVariants
 import Name
+import PPrint
 import Subst
 import QueryType
 import Types.Core
diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs
index b43b81a4..87a6e676 100644
--- a/src/lib/Types/Source.hs
+++ b/src/lib/Types/Source.hs
@@ -20,7 +20,7 @@
 
 module Types.Source where
 
-import Data.Aeson (ToJSON, ToJSONKey)
+import Data.Aeson (ToJSON)
 import Data.Hashable
 import Data.Foldable
 import qualified Data.Map.Strict       as M
@@ -61,13 +61,6 @@ newtype SourceOrInternalName (c::C) (n::S) = SourceOrInternalName (SourceNameOr
 
 -- === Source Info ===
 
--- XXX: 0 is reserved for the root The IDs are generated from left to right in
--- parsing order, so IDs for lexemes are guaranteed to be sorted correctly.
-newtype SrcId = SrcId Int  deriving (Show, Eq, Ord, Generic)
-
-rootSrcId :: SrcId
-rootSrcId = SrcId 0
-
 -- This is just for syntax highlighting. It won't be needed if we have
 -- a separate lexing pass where we have a complete lossless data type for
 -- lexemes.
@@ -959,14 +952,10 @@ deriving instance Show (UEffectRow n)
 deriving instance Eq   (UEffectRow n)
 deriving instance Ord  (UEffectRow n)
 
-instance ToJSON SrcId
-deriving instance ToJSONKey SrcId
 instance ToJSON LexemeType
 
 -- === Pretty instances ===
 
-
-
 instance Pretty CSBlock where
   pretty (IndentedBlock _ decls) = nest 2 $ prettyLines decls
   pretty (ExprBlock g) = pArg g
diff --git a/src/lib/Types/Top.hs b/src/lib/Types/Top.hs
index fba64b0e..b67fe357 100644
--- a/src/lib/Types/Top.hs
+++ b/src/lib/Types/Top.hs
@@ -71,15 +71,6 @@ data AtomBinding (r::IR) (n::S) where
 deriving instance IRRep r => Show (AtomBinding r n)
 deriving via WrapE (AtomBinding r) n instance IRRep r => Generic (AtomBinding r n)
 
--- name of function, name of arg
-type InferenceArgDesc = (String, String)
-data InfVarDesc =
-   ImplicitArgInfVar InferenceArgDesc
- | AnnotationInfVar String -- name of binder
- | TypeInstantiationInfVar String -- name of type
- | MiscInfVar
-   deriving (Show, Generic, Eq, Ord)
-
 data SolverBinding (n::S) =
    InfVarBound (CType n)
  | SkolemBound (CType n)
@@ -1023,7 +1014,6 @@ instance Pretty (SpecializationSpec n) where
   pretty (AppSpecialization f (Abs bs (ListE args))) =
     "Specialization" <+> pretty f <+> pretty bs <+> pretty args
 
-instance Hashable InfVarDesc
 instance Hashable a => Hashable (EvalStatus a)
 
 instance Store (SolverBinding n)
@@ -1039,7 +1029,6 @@ instance Store (TopFunDef n)
 instance Color c => Store (Binding c n)
 instance Store (ModuleEnv n)
 instance Store (SerializedEnv n)
-instance Store InfVarDesc
 instance Store (AtomRules n)
 instance Store (LinearizationSpec n)
 instance Store (SpecializedDictDef n)
diff --git a/src/lib/Vectorize.hs b/src/lib/Vectorize.hs
index 90e289df..daa606fc 100644
--- a/src/lib/Vectorize.hs
+++ b/src/lib/Vectorize.hs
@@ -117,7 +117,7 @@ liftTopVectorizeM vectorByteWidth action = do
     Success (a, (LiftE errs)) -> return $ (a, errs)
 
 throwVectErr :: Fallible m => String -> m a
-throwVectErr msg = throw MiscErr msg
+throwVectErr msg = throwInternal msg
 
 askVectorByteWidth :: TopVectorizeM i o Word32
 askVectorByteWidth = TopVectorizeM $ liftSubstReaderT $ lift11 (fromLiftE <$> ask)
@@ -581,7 +581,7 @@ promoteTypeByStability ty = \case
   Varying -> getVectorType ty
   ProdStability stabs -> case ty of
     TyCon (ProdType elts) -> TyCon <$> ProdType <$> zipWithZ promoteTypeByStability elts stabs
-    _ -> throw ZipErr "Type and stability"
+    _ -> throwInternal "Zip error"
 
 -- === computing byte widths ===