diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 93ffd88..6326a5e 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -13,6 +13,7 @@ import System.File
 import System.Path
 import Data.IORef
 
+import public Quox.Parser.FromParser.Error
 
 %default total
 
@@ -33,17 +34,6 @@ public export
 0 Defs : Type
 Defs = Definitions Three
 
-public export
-data FromParserError =
-    AnnotationNeeded PTerm
-  | DuplicatesInEnum (List TagVal)
-  | DimNotInScope PBaseName
-  | QtyNotGlobal PQty
-  | DimNameInTerm PBaseName
-  | TypeError (Typing.Error Three)
-  | LoadError String FileError
-  | ParseError Parser.Error
-
 public export
 0 IncludePath : Type
 IncludePath = List String
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
new file mode 100644
index 0000000..9f7a004
--- /dev/null
+++ b/lib/Quox/Parser/FromParser/Error.idr
@@ -0,0 +1,57 @@
+module Quox.Parser.FromParser.Error
+
+import Quox.Parser.Parser
+import Quox.Typing
+import System.File
+
+import Quox.Pretty
+
+
+public export
+data Error =
+    AnnotationNeeded PTerm
+  | DuplicatesInEnum (List TagVal)
+  | DimNotInScope PBaseName
+  | QtyNotGlobal PQty
+  | DimNameInTerm PBaseName
+  | TypeError (Typing.Error Three)
+  | LoadError String FileError
+  | ParseError Parser.Error
+%hide Typing.Error
+%hide Lexer.Error
+%hide Parser.Error
+
+
+parameters (unicode, showContext : Bool)
+  export
+  prettyError : Error -> Doc HL
+  prettyError (AnnotationNeeded tm) =
+    sep ["the term", "«PTerm»", -- pretty0 unicode tm,
+         "needs a type annotation"]
+
+  prettyError (DuplicatesInEnum tags) =
+    sep ["duplicate tags in enum type",
+         braces $ fillSep $ map pretty tags]
+
+  prettyError (DimNotInScope i) =
+    sep ["dimension", pretty0 unicode $ DV $ fromString i,
+         "not in scope"]
+
+  prettyError (QtyNotGlobal pi) =
+    sep ["quantity", pretty0 unicode pi,
+         "can't be used on a top level declaration"]
+
+  prettyError (DimNameInTerm i) =
+    sep ["dimension variable", pretty0 unicode $ DV $ fromString i,
+         "used in a term context"]
+
+  prettyError (TypeError err) =
+    Typing.prettyError unicode showContext $
+    trimContext 2 err
+
+  prettyError (LoadError str err) =
+    vsep [hsep ["couldn't load file", pretty str],
+          "«FileError»"]
+
+  prettyError (ParseError err) =
+    pretty $ show err
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index 16a31b2..f8b9496 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -6,7 +6,9 @@ import public Quox.Parser.Syntax
 import Data.Fin
 import Data.Vect
 import public Text.Parser
+import Derive.Prelude
 
+%language ElabReflection
 %default total
 
 
@@ -325,6 +327,7 @@ data Error =
     LexError   Lexer.Error
   | ParseError (List1 (ParsingError Token))
 %hide Lexer.Error
+%runElab derive "Error" [Show]
 
 export
 lexParseWith : {c : Bool} -> Grammar c a -> String -> Either Error a
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index e588c9a..9d87e7b 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -41,4 +41,5 @@ modules =
   Quox.Parser.Syntax,
   Quox.Parser.Parser,
   Quox.Parser.FromParser,
+  Quox.Parser.FromParser.Error,
   Quox.Parser