diff --git a/disco.cabal b/disco.cabal
index ea8031b1..0fd7885d 100644
--- a/disco.cabal
+++ b/disco.cabal
@@ -460,7 +460,7 @@ library
                        mtl >=2.2 && <2.4,
                        megaparsec >= 6.1.1 && < 9.6,
                        parser-combinators >= 1.0.0 && < 1.4,
-                       pretty >=1.1 && <1.2,
+                       prettyprinter >=1.7 && < 1.8,
                        split >= 0.2 && < 0.3,
                        transformers >= 0.4 && < 0.7,
                        containers >=0.5 && <0.7,
diff --git a/src/Disco/AST/Core.hs b/src/Disco/AST/Core.hs
index e8178646..877373ff 100644
--- a/src/Disco/AST/Core.hs
+++ b/src/Disco/AST/Core.hs
@@ -291,17 +291,15 @@ instance Pretty Core where
     CCase c l r -> do
       lunbind l $ \(x, lc) -> do
         lunbind r $ \(y, rc) -> do
-          "case"
-            <+> pretty c
-            <+> "of {"
-            $+$ nest
-              2
-              ( vcat
-                  [ withPA funPA $ "left" <+> rt (pretty x) <+> "->" <+> pretty lc
-                  , withPA funPA $ "right" <+> rt (pretty y) <+> "->" <+> pretty rc
-                  ]
-              )
-            $+$ "}"
+          nest 2 $
+            "case"
+              <+> pretty c
+              <+> "of {"
+              $+$ vcat
+                [ withPA funPA $ "left" <+> rt (pretty x) <+> "->" <+> pretty lc
+                , withPA funPA $ "right" <+> rt (pretty y) <+> "->" <+> pretty rc
+                ]
+              $+$ "}"
     CUnit -> "unit"
     CPair c1 c2 -> setPA initPA $ parens (pretty c1 <> ", " <> pretty c2)
     CProj s c -> withPA funPA $ selectSide s "fst" "snd" <+> rt (pretty c)
@@ -318,7 +316,7 @@ instance Pretty Core where
 toTuple :: [Core] -> Core
 toTuple = foldr CPair CUnit
 
-prettyTestVars :: Members '[Reader PA, LFresh] r => [(String, Type, Name Core)] -> Sem r Doc
+prettyTestVars :: Members '[Reader PA, LFresh] r => [(String, Type, Name Core)] -> Sem r (Doc ann)
 prettyTestVars = brackets . intercalate "," . map prettyTestVar
  where
   prettyTestVar (s, ty, n) = parens (intercalate "," [text s, pretty ty, pretty n])
diff --git a/src/Disco/AST/Surface.hs b/src/Disco/AST/Surface.hs
index c15c43e8..7646e8d9 100644
--- a/src/Disco/AST/Surface.hs
+++ b/src/Disco/AST/Surface.hs
@@ -2,10 +2,6 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
 
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- |
 -- Module      :  Disco.AST.Surface
 -- Copyright   :  disco team and contributors
@@ -236,7 +232,7 @@ instance Pretty (Name a, Bind [Pattern] Term) where
     pretty x <> hcat (map prettyPatternP ps) <+> text "=" <+> setPA initPA (pretty t)
 
 -- | Pretty-print a type declaration.
-prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r Doc
+prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r (Doc ann)
 prettyTyDecl x ty = hsep [pretty x, text ":", pretty ty]
 
 ------------------------------------------------------------
@@ -526,7 +522,7 @@ pattern PNonlinear p x <- PNonlinear_ (unembed -> p) x
 -- term (e.g. via the :doc REPL command).
 
 -- | Pretty-print a term with guaranteed parentheses.
-prettyTermP :: Members '[LFresh, Reader PA] r => Term -> Sem r Doc
+prettyTermP :: Members '[LFresh, Reader PA] r => Term -> Sem r (Doc ann)
 prettyTermP t@TTup {} = setPA initPA $ pretty t
 -- prettyTermP t@TContainer{} = setPA initPA $ "" <+> prettyTerm t
 prettyTermP t = withPA initPA $ pretty t
@@ -630,12 +626,12 @@ instance Pretty Term where
     TWild -> text "_"
 
 -- | Print appropriate delimiters for a container literal.
-containerDelims :: Member (Reader PA) r => Container -> (Sem r Doc -> Sem r Doc)
+containerDelims :: Member (Reader PA) r => Container -> (Sem r (Doc ann) -> Sem r (Doc ann))
 containerDelims ListContainer = brackets
 containerDelims BagContainer = bag
 containerDelims SetContainer = braces
 
-prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r Doc
+prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r (Doc ann)
 prettyBranches = \case
   [] -> error "Empty branches are disallowed."
   b : bs ->
@@ -681,7 +677,7 @@ instance Pretty Qual where
     QGuard (unembed -> t) -> pretty t
 
 -- | Pretty-print a pattern with guaranteed parentheses.
-prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r Doc
+prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r (Doc ann)
 prettyPatternP p@PTup {} = setPA initPA $ pretty p
 prettyPatternP p = withPA initPA $ pretty p
 
diff --git a/src/Disco/Error.hs b/src/Disco/Error.hs
index 6282d0eb..c80fbf42 100644
--- a/src/Disco/Error.hs
+++ b/src/Disco/Error.hs
@@ -82,7 +82,7 @@ deriving instance Show EvalError
 panic :: Member (Error DiscoError) r => String -> Sem r a
 panic = throw . Panic
 
-outputDiscoErrors :: Member (Output Message) r => Sem (Error DiscoError ': r) () -> Sem r ()
+outputDiscoErrors :: Member (Output (Message ann)) r => Sem (Error DiscoError ': r) () -> Sem r ()
 outputDiscoErrors m = do
   e <- runError m
   either (err . pretty') return e
@@ -93,9 +93,9 @@ instance Pretty DiscoError where
     CyclicImport ms -> cyclicImportError ms
     TypeCheckErr (LocTCError Nothing te) -> prettyTCError te
     TypeCheckErr (LocTCError (Just n) te) ->
-      vcat
+      nest 2 $ vcat
         [ "While checking " <> pretty' n <> ":"
-        , nest 2 $ prettyTCError te
+        , prettyTCError te
         ]
     ParseErr pe -> text (errorBundlePretty pe)
     EvalErr ee -> prettyEvalError ee
@@ -105,23 +105,23 @@ instance Pretty DiscoError where
         , "Please report this as a bug at https://github.com/disco-lang/disco/issues/ ."
         ]
 
-rtd :: String -> Sem r Doc
+rtd :: String -> Sem r (Doc ann)
 rtd page = "https://disco-lang.readthedocs.io/en/latest/reference/" <> text page <> ".html"
 
-issue :: Int -> Sem r Doc
+issue :: Int -> Sem r (Doc ann)
 issue n = "See https://github.com/disco-lang/disco/issues/" <> text (show n)
 
 cyclicImportError ::
   Members '[Reader PA, LFresh] r =>
   [ModuleName] ->
-  Sem r Doc
+  Sem r (Doc ann)
 cyclicImportError ms =
-  vcat
+  nest 2 $ vcat
     [ "Error: module imports form a cycle:"
-    , nest 2 $ intercalate " ->" (map pretty ms)
+    , intercalate " ->" (map pretty ms)
     ]
 
-prettyEvalError :: Members '[Reader PA, LFresh] r => EvalError -> Sem r Doc
+prettyEvalError :: Members '[Reader PA, LFresh] r => EvalError -> Sem r (Doc ann)
 prettyEvalError = \case
   UnboundPanic x ->
     ("Bug! No variable found named" <+> pretty' x <> ".")
@@ -138,7 +138,7 @@ prettyEvalError = \case
 -- [ ] Step 3: improve error messages according to notes below
 -- [ ] Step 4: get it to return multiple error messages
 -- [ ] Step 5: save parse locations, display with errors
-prettyTCError :: Members '[Reader PA, LFresh] r => TCError -> Sem r Doc
+prettyTCError :: Members '[Reader PA, LFresh] r => TCError -> Sem r (Doc ann)
 prettyTCError = \case
   -- XXX include some potential misspellings along with Unbound
   --   see https://github.com/disco-lang/disco/issues/180
@@ -150,7 +150,7 @@ prettyTCError = \case
   Ambiguous x ms ->
     vcat
       [ "Error: the name" <+> pretty' x <+> "is ambiguous. It could refer to:"
-      , nest 2 (vcat . map (\m -> pretty' m <> "." <> pretty' x) $ ms)
+      , indent 2 . vcat . map (\m -> pretty' m <> "." <> pretty' x) $ ms
       , rtd "ambiguous"
       ]
   NoType x ->
@@ -166,9 +166,9 @@ prettyTCError = \case
   NotCon c t ty ->
     vcat
       [ "Error: the expression"
-      , nest 2 $ pretty' t
+      , indent 2 $ pretty' t
       , "must have both a" <+> conWord c <+> "type and also the incompatible type"
-      , nest 2 $ pretty' ty <> "."
+      , indent 2 $ pretty' ty <> "."
       , rtd "notcon"
       ]
   EmptyCase ->
@@ -179,9 +179,9 @@ prettyTCError = \case
   PatternType c pat ty ->
     vcat
       [ "Error: the pattern"
-      , nest 2 $ pretty' pat
+      , indent 2 $ pretty' pat
       , "is supposed to have type"
-      , nest 2 $ pretty' ty <> ","
+      , indent 2 $ pretty' ty <> ","
       , "but instead it has a" <+> conWord c <+> "type."
       , rtd "pattern-type"
       ]
@@ -220,7 +220,7 @@ prettyTCError = \case
   NoSearch ty ->
     vcat
       [ "Error: the type"
-      , nest 2 $ pretty' ty
+      , indent 2 $ pretty' ty
       , "is not searchable (i.e. it cannot be used in a forall)."
       , rtd "no-search"
       ]
@@ -259,7 +259,7 @@ prettyTCError = \case
   NoPolyRec s ss tys ->
     vcat
       [ "Error: in the definition of " <> text s <> parens (intercalate "," (map text ss)) <> ": recursive occurrences of" <+> text s <+> "may only have type variables as arguments."
-      , nest
+      , indent
           2
           ( text s <> parens (intercalate "," (map pretty' tys)) <+> "does not follow this rule."
           )
@@ -267,7 +267,7 @@ prettyTCError = \case
       ]
   NoError -> empty
 
-conWord :: Con -> Sem r Doc
+conWord :: Con -> Sem r (Doc ann)
 conWord = \case
   CArr -> "function"
   CProd -> "pair"
@@ -280,7 +280,7 @@ conWord = \case
   CGraph -> "graph"
   CUser s -> text s
 
-prettySolveError :: Members '[Reader PA, LFresh] r => SolveError -> Sem r Doc
+prettySolveError :: Members '[Reader PA, LFresh] r => SolveError -> Sem r (Doc ann)
 prettySolveError = \case
   -- XXX say which types!
   NoWeakUnifier ->
@@ -307,16 +307,16 @@ prettySolveError = \case
   QualSkolem q a ->
     vcat
       [ "Error: type variable" <+> pretty' a <+> "represents any type, so we cannot assume values of that type"
-      , nest 2 (qualPhrase True q) <> "."
+      , indent 2 (qualPhrase True q) <> "."
       , rtd "qual-skolem"
       ]
 
-qualPhrase :: Bool -> Qualifier -> Sem r Doc
+qualPhrase :: Bool -> Qualifier -> Sem r (Doc ann)
 qualPhrase b q
   | q `elem` [QBool, QBasic, QSimple] = "are" <+> (if b then empty else "not") <+> qualAction q
   | otherwise = "can" <> (if b then empty else "not") <+> "be" <+> qualAction q
 
-qualAction :: Qualifier -> Sem r Doc
+qualAction :: Qualifier -> Sem r (Doc ann)
 qualAction = \case
   QNum -> "added and multiplied"
   QSub -> "subtracted"
diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs
index b246dbd0..b5ddd356 100644
--- a/src/Disco/Eval.hs
+++ b/src/Disco/Eval.hs
@@ -2,10 +2,6 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- |
 -- Module      :  Disco.Eval
 -- Copyright   :  disco team and contributors
@@ -164,10 +160,10 @@ type family AppendEffects (r :: EffectRow) (s :: EffectRow) :: EffectRow where
 -- However, just manually implementing it here seems easier.
 
 -- | Effects needed at the top level.
-type TopEffects = '[Error DiscoError, State TopInfo, Output Message, Embed IO, Final (H.InputT IO)]
+type TopEffects = '[Error DiscoError, State TopInfo, Output (Message ()), Embed IO, Final (H.InputT IO)]
 
 -- | Effects needed for evaluation.
-type EvalEffects = [Error EvalError, Random, LFresh, Output Message, State Mem]
+type EvalEffects = [Error EvalError, Random, LFresh, Output (Message ()), State Mem]
 
 -- XXX write about order.
 -- memory, counter etc. should not be reset by errors.
@@ -296,7 +292,7 @@ typecheckTop tcm = do
 --   The 'Resolver' argument specifies where to look for imported
 --   modules.
 loadDiscoModule ::
-  Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r =>
+  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>
   Bool ->
   Resolver ->
   FilePath ->
@@ -310,7 +306,7 @@ loadDiscoModule quiet resolver =
 --   module loaded from disk).  Used for e.g. blocks/modules entered
 --   at the REPL prompt.
 loadParsedDiscoModule ::
-  Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r =>
+  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>
   Bool ->
   Resolver ->
   ModuleName ->
@@ -324,7 +320,7 @@ loadParsedDiscoModule quiet resolver =
 --   any imported module more than once. Resolve the module, load and
 --   parse it, then call 'loadParsedDiscoModule''.
 loadDiscoModule' ::
-  Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r =>
+  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>
   Bool ->
   Resolver ->
   [ModuleName] ->
@@ -356,7 +352,7 @@ stdLib = ["list", "container"]
 --   'LoadingMode' parameter is 'REPL'.  Recursively load all its
 --   imports, then typecheck it.
 loadParsedDiscoModule' ::
-  Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r =>
+  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>
   Bool ->
   LoadingMode ->
   Resolver ->
@@ -398,7 +394,7 @@ loadParsedDiscoModule' quiet mode resolver inProcess name cm@(Module _ mns _ _ _
 
 -- | Try loading the contents of a file from the filesystem, emitting
 --   an error if it's not found.
-loadFile :: Members '[Output Message, Embed IO] r => FilePath -> Sem r (Maybe String)
+loadFile :: Members '[Output (Message ann), Embed IO] r => FilePath -> Sem r (Maybe String)
 loadFile file = do
   res <- liftIO $ handle @SomeException (return . Left) (Right <$> readFile file)
   case res of
@@ -408,7 +404,7 @@ loadFile file = do
 -- | Add things from the given module to the set of currently loaded
 --   things.
 addToREPLModule ::
-  Members '[Error DiscoError, State TopInfo, Random, State Mem, Output Message] r =>
+  Members '[Error DiscoError, State TopInfo, Random, State Mem, Output (Message ann)] r =>
   ModuleInfo ->
   Sem r ()
 addToREPLModule mi = modify @TopInfo (replModInfo <>~ mi)
@@ -418,7 +414,7 @@ addToREPLModule mi = modify @TopInfo (replModInfo <>~ mi)
 --   term definitions, documentation, types, and type definitions.
 --   Replaces any previously loaded module.
 setREPLModule ::
-  Members '[State TopInfo, Random, Error EvalError, State Mem, Output Message] r =>
+  Members '[State TopInfo, Random, Error EvalError, State Mem, Output (Message ann)] r =>
   ModuleInfo ->
   Sem r ()
 setREPLModule mi = do
diff --git a/src/Disco/Interactive/Commands.hs b/src/Disco/Interactive/Commands.hs
index acf10c38..68409000 100644
--- a/src/Disco/Interactive/Commands.hs
+++ b/src/Disco/Interactive/Commands.hs
@@ -2,10 +2,6 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE StandaloneDeriving #-}
 
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- |
 -- Module      :  Disco.Interactive.Commands
 -- Copyright   :  disco team and contributors
@@ -84,7 +80,7 @@ import Disco.Parser (
   withExts,
  )
 import Disco.Pretty hiding (empty, (<>))
-import qualified Disco.Pretty as Pretty
+import qualified Disco.Pretty as PP
 import Disco.Property (prettyTestResult)
 import Disco.Syntax.Operators
 import Disco.Syntax.Prims (
@@ -303,7 +299,7 @@ annCmd =
     }
 
 handleAnn ::
-  Members '[Error DiscoError, Input TopInfo, Output Message] r =>
+  Members '[Error DiscoError, Input TopInfo, Output (Message ())] r =>
   REPLExpr 'CAnn ->
   Sem r ()
 handleAnn (Ann t) = do
@@ -326,7 +322,7 @@ compileCmd =
     }
 
 handleCompile ::
-  Members '[Error DiscoError, Input TopInfo, Output Message] r =>
+  Members '[Error DiscoError, Input TopInfo, Output (Message ())] r =>
   REPLExpr 'CCompile ->
   Sem r ()
 handleCompile (Compile t) = do
@@ -349,7 +345,7 @@ desugarCmd =
     }
 
 handleDesugar ::
-  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
+  Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
   REPLExpr 'CDesugar ->
   Sem r ()
 handleDesugar (Desugar t) = do
@@ -383,7 +379,7 @@ parseDoc =
     <|> (DocOther <$> (sc *> many (anySingleBut ' ')))
 
 handleDoc ::
-  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
+  Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
   REPLExpr 'CDoc ->
   Sem r ()
 handleDoc (Doc (DocTerm (TBool _))) = handleDocBool
@@ -396,26 +392,26 @@ handleDoc (Doc (DocTerm _)) =
 handleDoc (Doc (DocPrim p)) = handleDocPrim p
 handleDoc (Doc (DocOther s)) = handleDocOther s
 
-handleDocBool :: Members '[Output Message] r => Sem r ()
+handleDocBool :: Members '[Output (Message ())] r => Sem r ()
 handleDocBool =
   info $
     "true and false (also written True and False) are the two possible values of type Boolean."
       $+$ mkReference "bool"
 
-handleDocUnit :: Members '[Output Message] r => Sem r ()
+handleDocUnit :: Members '[Output (Message ())] r => Sem r ()
 handleDocUnit =
   info $
     "The unit value, i.e. the single value of type Unit."
       $+$ mkReference "unit"
 
-handleDocWild :: Members '[Output Message] r => Sem r ()
+handleDocWild :: Members '[Output (Message ())] r => Sem r ()
 handleDocWild =
   info $
     "A wildcard pattern."
       $+$ mkReference "wild-pattern"
 
 handleDocVar ::
-  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
+  Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
   Name Term ->
   Sem r ()
 handleDocVar x = do
@@ -447,60 +443,67 @@ handleDocVar x = do
       hsep [pretty' x, ":", pretty' ty]
         $+$ case Ctx.lookup' qn docMap of
           Just (DocString ss : _) -> vcat (text "" : map text ss ++ [text ""])
-          _ -> Pretty.empty
+          _ -> PP.empty
   showDoc docMap (Right tdBody) =
     info $
       pretty' (name2String x, tdBody)
         $+$ case Ctx.lookupAll' x docMap of
           ((_, DocString ss : _) : _) -> vcat (text "" : map text ss ++ [text ""])
-          _ -> Pretty.empty
+          _ -> PP.empty
 
 handleDocPrim ::
-  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
+  Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
   Prim ->
   Sem r ()
 handleDocPrim prim = do
   handleTypeCheck (TypeCheck (TPrim prim))
-  info $
-    vcat
-      [ case prim of
+  info
+    . vcat
+    $ ( case prim of
           PrimUOp u -> describeAlts (f == Post) (f == Pre) syns
            where
             OpInfo (UOpF f _) syns _ = uopMap ! u
           PrimBOp b -> describeAlts True True (opSyns $ bopMap ! b)
-          _ -> Pretty.empty
-      , case prim of
-          PrimUOp u -> describePrec (uPrec u)
-          PrimBOp b -> describePrec (bPrec b) <> describeFixity (assoc b)
-          _ -> Pretty.empty
-      ]
+          _ -> []
+      )
+      ++ ( case prim of
+            PrimUOp u -> [describePrec (uPrec u)]
+            PrimBOp b -> [describePrec (bPrec b) <> describeFixity (assoc b)]
+            _ -> []
+         )
   case (M.lookup prim primDoc, M.lookup prim primReference) of
     (Nothing, Nothing) -> return ()
     (Nothing, Just p) -> info $ mkReference p
     (Just d, mp) ->
-      info $ "" $+$ text d $+$ "" $+$ maybe Pretty.empty (\p -> mkReference p $+$ "") mp
+      info $
+        vcat
+          [ PP.empty
+          , text d
+          , PP.empty
+          , maybe PP.empty (\p -> vcat [mkReference p, PP.empty]) mp
+          ]
  where
   describePrec p = "precedence level" <+> text (show p)
-  describeFixity In = Pretty.empty
+  describeFixity In = PP.empty
   describeFixity InL = ", left associative"
   describeFixity InR = ", right associative"
-  describeAlts _ _ [] = Pretty.empty
-  describeAlts _ _ [_] = Pretty.empty
-  describeAlts pre post (_ : alts) = "Alternative syntax:" <+> intercalate "," (map showOp alts)
+  describeAlts _ _ [] = []
+  describeAlts _ _ [_] = []
+  describeAlts pre post (_ : alts) = ["Alternative syntax:" <+> intercalate "," (map showOp alts)]
    where
     showOp op =
       hcat
-        [ if pre then "~" else Pretty.empty
+        [ if pre then "~" else PP.empty
         , text op
-        , if post then "~" else Pretty.empty
+        , if post then "~" else PP.empty
         ]
 
-mkReference :: String -> Sem r Doc
+mkReference :: String -> Sem r (Doc ann)
 mkReference p =
   "https://disco-lang.readthedocs.io/en/latest/reference/" <> text p <> ".html"
 
 handleDocOther ::
-  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
+  Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
   String ->
   Sem r ()
 handleDocOther s =
@@ -508,7 +511,12 @@ handleDocOther s =
     (Nothing, Nothing) -> info $ "No documentation found for '" <> text s <> "'."
     (Nothing, Just p) -> info $ mkReference p
     (Just d, mp) ->
-      info $ text d $+$ "" $+$ maybe Pretty.empty (\p -> mkReference p $+$ "") mp
+      info $
+        vcat
+          [ text d
+          , PP.empty
+          , maybe PP.empty (\p -> vcat [mkReference p, PP.empty]) mp
+          ]
 
 ------------------------------------------------------------
 -- eval
@@ -526,7 +534,7 @@ evalCmd =
     }
 
 handleEval ::
-  Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
+  Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r =>
   REPLExpr 'CEval ->
   Sem r ()
 handleEval (Eval m) = do
@@ -537,7 +545,7 @@ handleEval (Eval m) = do
 -- garbageCollect?
 
 -- First argument = should the value be printed?
-evalTerm :: Members (Error EvalError ': State TopInfo ': Output Message ': EvalEffects) r => Bool -> ATerm -> Sem r Value
+evalTerm :: Members (Error EvalError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => Bool -> ATerm -> Sem r Value
 evalTerm pr at = do
   env <- use @TopInfo topEnv
   v <- runInputConst env $ eval (compileTerm at)
@@ -567,7 +575,7 @@ helpCmd =
     , parser = return Help
     }
 
-handleHelp :: Member (Output Message) r => REPLExpr 'CHelp -> Sem r ()
+handleHelp :: Member (Output (Message ())) r => REPLExpr 'CHelp -> Sem r ()
 handleHelp Help =
   info $
     vcat
@@ -606,13 +614,13 @@ loadCmd =
 --   in the parent module are executed.
 --   Disco.Interactive.CmdLine uses a version of this function that returns a Bool.
 handleLoadWrapper ::
-  Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
+  Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r =>
   REPLExpr 'CLoad ->
   Sem r ()
 handleLoadWrapper (Load fp) = void (handleLoad fp)
 
 handleLoad ::
-  Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
+  Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r =>
   FilePath ->
   Sem r Bool
 handleLoad fp = do
@@ -640,7 +648,7 @@ handleLoad fp = do
 
 -- XXX Return a structured summary of the results, not a Bool; & move
 -- this somewhere else?
-runAllTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => [QName Term] -> Ctx ATerm [AProperty] -> Sem r Bool -- (Ctx ATerm [TestResult])
+runAllTests :: Members (Output (Message ()) ': Input TopInfo ': EvalEffects) r => [QName Term] -> Ctx ATerm [AProperty] -> Sem r Bool -- (Ctx ATerm [TestResult])
 runAllTests declNames aprops
   | Ctx.null aprops = return True
   | otherwise = do
@@ -650,21 +658,23 @@ runAllTests declNames aprops
  where
   numSamples :: Int
   numSamples = 50 -- XXX make this configurable somehow
-  runTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => QName Term -> [AProperty] -> Sem r Bool
+  runTests :: Members (Output (Message ()) ': Input TopInfo ': EvalEffects) r => QName Term -> [AProperty] -> Sem r Bool
   runTests (QName _ n) props = do
     results <- inputTopEnv $ traverse (sequenceA . (id &&& runTest numSamples)) props
     let failures = P.filter (not . testIsOk . snd) results
         hdr = pretty' n <> ":"
 
     case P.null failures of
-      True -> info $ nest 2 $ hdr <+> "OK"
+      True -> info $ indent 2 $ hdr <+> "OK"
       False -> do
         tydefs <- inputs @TopInfo (view (replModInfo . to allTydefs))
         let prettyFailures =
-              runInputConst tydefs . runReader initPA . runLFresh $
-                bulletList "-" $
-                  map (uncurry prettyTestResult) failures
-        info $ nest 2 $ hdr $+$ prettyFailures
+              runInputConst tydefs
+                . runReader initPA
+                . runLFresh
+                $ bulletList "-"
+                $ map (uncurry prettyTestResult) failures
+        info $ indent 2 $ hdr $+$ prettyFailures
     return (P.null failures)
 
 ------------------------------------------------------------
@@ -684,7 +694,7 @@ namesCmd =
 
 -- | Show names and types for each item in the top-level context.
 handleNames ::
-  Members '[Input TopInfo, LFresh, Output Message] r =>
+  Members '[Input TopInfo, LFresh, Output (Message ())] r =>
   REPLExpr 'CNames ->
   Sem r ()
 handleNames Names = do
@@ -729,7 +739,7 @@ parseCmd =
     , parser = Parse <$> term
     }
 
-handleParse :: Member (Output Message) r => REPLExpr 'CParse -> Sem r ()
+handleParse :: Member (Output (Message ())) r => REPLExpr 'CParse -> Sem r ()
 handleParse (Parse t) = info (text (show t))
 
 ------------------------------------------------------------
@@ -747,7 +757,7 @@ prettyCmd =
     , parser = Pretty <$> term
     }
 
-handlePretty :: Members '[LFresh, Output Message] r => REPLExpr 'CPretty -> Sem r ()
+handlePretty :: Members '[LFresh, Output (Message ())] r => REPLExpr 'CPretty -> Sem r ()
 handlePretty (Pretty t) = info $ pretty' t
 
 ------------------------------------------------------------
@@ -765,7 +775,7 @@ printCmd =
     , parser = Print <$> term
     }
 
-handlePrint :: Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r => REPLExpr 'CPrint -> Sem r ()
+handlePrint :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CPrint -> Sem r ()
 handlePrint (Print t) = do
   at <- inputToState . typecheckTop $ checkTop t (toPolyType TyString)
   v <- mapError EvalErr . evalTerm False $ at
@@ -787,7 +797,7 @@ reloadCmd =
     }
 
 handleReload ::
-  Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
+  Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r =>
   REPLExpr 'CReload ->
   Sem r ()
 handleReload Reload = do
@@ -812,7 +822,7 @@ showDefnCmd =
     }
 
 handleShowDefn ::
-  Members '[Input TopInfo, LFresh, Output Message] r =>
+  Members '[Input TopInfo, LFresh, Output (Message ())] r =>
   REPLExpr 'CShowDefn ->
   Sem r ()
 handleShowDefn (ShowDefn x) = do
@@ -845,7 +855,7 @@ testPropCmd =
     }
 
 handleTest ::
-  Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r =>
+  Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r =>
   REPLExpr 'CTestProp ->
   Sem r ()
 handleTest (TestProp t) = do
@@ -853,7 +863,7 @@ handleTest (TestProp t) = do
   tydefs <- use @TopInfo (replModInfo . to allTydefs)
   inputToState . inputTopEnv $ do
     r <- runTest 100 at -- XXX make configurable
-    info $ runInputConst tydefs . runReader initPA $ nest 2 $ "-" <+> prettyTestResult at r
+    info $ runInputConst tydefs . runReader initPA $ indent 2 . nest 2 $ "-" <+> prettyTestResult at r
 
 ------------------------------------------------------------
 -- :type
@@ -871,7 +881,7 @@ typeCheckCmd =
     }
 
 handleTypeCheck ::
-  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
+  Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
   REPLExpr 'CTypeCheck ->
   Sem r ()
 handleTypeCheck (TypeCheck t) = do
diff --git a/src/Disco/Messages.hs b/src/Disco/Messages.hs
index 4e5ea677..afacd7d1 100644
--- a/src/Disco/Messages.hs
+++ b/src/Disco/Messages.hs
@@ -30,34 +30,34 @@ data MessageType
   | Debug
   deriving (Show, Read, Eq, Ord, Enum, Bounded)
 
-data Message = Message {_messageType :: MessageType, _message :: Doc}
+data Message ann = Message {_messageType :: MessageType, _message :: (Doc ann)}
   deriving (Show)
 
 makeLenses ''Message
 
-handleMsg :: Member (Embed IO) r => (Message -> Bool) -> Message -> Sem r ()
+handleMsg :: Member (Embed IO) r => (Message ann -> Bool) -> Message ann -> Sem r ()
 handleMsg p m = when (p m) $ printMsg m
 
-printMsg :: Member (Embed IO) r => Message -> Sem r ()
+printMsg :: Member (Embed IO) r => Message ann -> Sem r ()
 printMsg (Message _ m) = embed $ putStrLn (renderDoc' m)
 
-msg :: Member (Output Message) r => MessageType -> Sem r Doc -> Sem r ()
+msg :: Member (Output (Message ann)) r => MessageType -> Sem r (Doc ann) -> Sem r ()
 msg typ m = m >>= output . Message typ
 
-info :: Member (Output Message) r => Sem r Doc -> Sem r ()
+info :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r ()
 info = msg Info
 
-infoPretty :: (Member (Output Message) r, Pretty t) => t -> Sem r ()
+infoPretty :: (Member (Output (Message ann)) r, Pretty t) => t -> Sem r ()
 infoPretty = info . pretty'
 
-warn :: Member (Output Message) r => Sem r Doc -> Sem r ()
+warn :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r ()
 warn = msg Warning
 
-debug :: Member (Output Message) r => Sem r Doc -> Sem r ()
+debug :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r ()
 debug = msg Debug
 
-debugPretty :: (Member (Output Message) r, Pretty t) => t -> Sem r ()
+debugPretty :: (Member (Output (Message ann)) r, Pretty t) => t -> Sem r ()
 debugPretty = debug . pretty'
 
-err :: Member (Output Message) r => Sem r Doc -> Sem r ()
+err :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r ()
 err = msg ErrMsg
diff --git a/src/Disco/Parser.hs b/src/Disco/Parser.hs
index 96d2b2d6..196c274e 100644
--- a/src/Disco/Parser.hs
+++ b/src/Disco/Parser.hs
@@ -1,9 +1,5 @@
 {-# LANGUAGE TemplateHaskell #-}
 
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- |
 -- Module      :  Disco.Parser
 -- Copyright   :  disco team and contributors
diff --git a/src/Disco/Pretty.hs b/src/Disco/Pretty.hs
index 981b869e..bcc47ed7 100644
--- a/src/Disco/Pretty.hs
+++ b/src/Disco/Pretty.hs
@@ -2,10 +2,6 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- TODO: the calls to 'error' should be replaced with logging/error capabilities.
 
 -- |
@@ -33,18 +29,14 @@ import qualified Data.Map as M
 import Data.Ratio
 import Data.Set (Set)
 import qualified Data.Set as S
-
 import Disco.Effects.LFresh
-import Polysemy
-
-import Polysemy.Reader
-
-import Text.PrettyPrint (Doc)
-import Unbound.Generics.LocallyNameless (Name)
-
 import Disco.Pretty.DSL
 import Disco.Pretty.Prec
 import Disco.Syntax.Operators
+import Polysemy
+import Polysemy.Reader
+import Prettyprinter (Doc)
+import Unbound.Generics.LocallyNameless (Name)
 
 ------------------------------------------------------------
 -- Utilities for handling precedence and associativity
@@ -54,7 +46,7 @@ import Disco.Syntax.Operators
 --   associativity of a term is, and optionally surround it with
 --   parentheses depending on the precedence and associativity of its
 --   parent.
-withPA :: Member (Reader PA) r => PA -> Sem r Doc -> Sem r Doc
+withPA :: Member (Reader PA) r => PA -> Sem r (Doc ann) -> Sem r (Doc ann)
 withPA pa = mparens pa . setPA pa
 
 -- | Locally set the precedence and associativity within a
@@ -65,20 +57,20 @@ setPA = local . const
 -- | Mark a subcomputation as pretty-printing a term on the left of an
 --   operator (so parentheses can be inserted appropriately, depending
 --   on the associativity).
-lt :: Member (Reader PA) r => Sem r Doc -> Sem r Doc
+lt :: Member (Reader PA) r => Sem r (Doc ann) -> Sem r (Doc ann)
 lt = local (\(PA p _) -> PA p InL)
 
 -- | Mark a subcomputation as pretty-printing a term on the right of
 --   an operator (so parentheses can be inserted appropriately,
 --   depending on the associativity).
-rt :: Member (Reader PA) r => Sem r Doc -> Sem r Doc
+rt :: Member (Reader PA) r => Sem r (Doc ann) -> Sem r (Doc ann)
 rt = local (\(PA p _) -> PA p InR)
 
 -- | Optionally surround a pretty-printed term with parentheses,
 --   depending on its precedence and associativity (given as the 'PA'
 --   argument) and that of its context (given by the ambient 'Reader
 --   PA' effect).
-mparens :: Member (Reader PA) r => PA -> Sem r Doc -> Sem r Doc
+mparens :: Member (Reader PA) r => PA -> Sem r (Doc ann) -> Sem r (Doc ann)
 mparens pa doc = do
   parentPA <- ask
   (if pa < parentPA then parens else id) doc
@@ -87,12 +79,12 @@ mparens pa doc = do
 -- Pretty type class
 
 class Pretty t where
-  pretty :: Members '[Reader PA, LFresh] r => t -> Sem r Doc
+  pretty :: Members '[Reader PA, LFresh] r => t -> Sem r (Doc ann)
 
 prettyStr :: Pretty t => t -> Sem r String
 prettyStr = renderDoc . runLFresh . pretty
 
-pretty' :: Pretty t => t -> Sem r Doc
+pretty' :: Pretty t => t -> Sem r (Doc ann)
 pretty' = runReader initPA . runLFresh . pretty
 
 ------------------------------------------------------------
diff --git a/src/Disco/Pretty/DSL.hs b/src/Disco/Pretty/DSL.hs
index 8032f150..dd7a2018 100644
--- a/src/Disco/Pretty/DSL.hs
+++ b/src/Disco/Pretty/DSL.hs
@@ -1,5 +1,3 @@
------------------------------------------------------------------------------
------------------------------------------------------------------------------
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 -- |
@@ -14,17 +12,16 @@ module Disco.Pretty.DSL where
 
 import Control.Applicative hiding (empty)
 import Data.String (IsString (..))
-import Prelude hiding ((<>))
-
+import Disco.Pretty.Prec
 import Polysemy
 import Polysemy.Reader
+import Prettyprinter (Doc)
+import qualified Prettyprinter as PP
+import Prettyprinter.Internal (Doc (Empty)) -- XXX comment me
+import Prettyprinter.Render.String (renderString)
+import Prelude hiding ((<>))
 
-import Text.PrettyPrint (Doc)
-import qualified Text.PrettyPrint as PP
-
-import Disco.Pretty.Prec
-
-instance IsString (Sem r Doc) where
+instance IsString (Sem r (Doc ann)) where
   fromString = text
 
 ------------------------------------------------------------
@@ -33,73 +30,79 @@ instance IsString (Sem r Doc) where
 -- Each combinator here mirrors one from Text.PrettyPrint, but
 -- operates over a generic functor/monad.
 
-vcat :: Applicative f => [f Doc] -> f Doc
+vcat :: Applicative f => [f (Doc ann)] -> f (Doc ann)
 vcat ds = PP.vcat <$> sequenceA ds
 
-hcat :: Applicative f => [f Doc] -> f Doc
+hcat :: Applicative f => [f (Doc ann)] -> f (Doc ann)
 hcat ds = PP.hcat <$> sequenceA ds
 
-hsep :: Applicative f => [f Doc] -> f Doc
+hsep :: Applicative f => [f (Doc ann)] -> f (Doc ann)
 hsep ds = PP.hsep <$> sequenceA ds
 
-parens :: Functor f => f Doc -> f Doc
+parens :: Functor f => f (Doc ann) -> f (Doc ann)
 parens = fmap PP.parens
 
-brackets :: Functor f => f Doc -> f Doc
+brackets :: Functor f => f (Doc ann) -> f (Doc ann)
 brackets = fmap PP.brackets
 
-braces :: Functor f => f Doc -> f Doc
+braces :: Functor f => f (Doc ann) -> f (Doc ann)
 braces = fmap PP.braces
 
-bag :: Applicative f => f Doc -> f Doc
+bag :: Applicative f => f (Doc ann) -> f (Doc ann)
 bag p = text "⟅" <> p <> text "⟆"
 
-quotes :: Functor f => f Doc -> f Doc
-quotes = fmap PP.quotes
+quotes :: Functor f => f (Doc ann) -> f (Doc ann)
+quotes = fmap PP.squotes
 
-doubleQuotes :: Functor f => f Doc -> f Doc
-doubleQuotes = fmap PP.doubleQuotes
+doubleQuotes :: Functor f => f (Doc ann) -> f (Doc ann)
+doubleQuotes = fmap PP.dquotes
 
-text :: Applicative m => String -> m Doc
-text = pure . PP.text
+text :: Applicative m => String -> m (Doc ann)
+text = pure . fromString
 
-integer :: Applicative m => Integer -> m Doc
-integer = pure . PP.integer
+integer :: Applicative m => Integer -> m (Doc ann)
+integer = pure . PP.pretty
 
-nest :: Functor f => Int -> f Doc -> f Doc
+nest :: Functor f => Int -> f (Doc ann) -> f (Doc ann)
 nest n d = PP.nest n <$> d
 
-hang :: Applicative f => f Doc -> Int -> f Doc -> f Doc
-hang d1 n d2 = PP.hang <$> d1 <*> pure n <*> d2
+indent :: Functor f => Int -> f (Doc ann) -> f (Doc ann)
+indent n d = PP.indent n <$> d
+
+hang :: Applicative f => f (Doc ann) -> Int -> f (Doc ann) -> f (Doc ann)
+hang d1 n d2 = d1 <+> nest n d2
 
-empty :: Applicative m => m Doc
-empty = pure PP.empty
+empty :: Applicative m => m (Doc ann)
+empty = pure PP.emptyDoc
 
-(<+>) :: Applicative f => f Doc -> f Doc -> f Doc
+(<+>) :: Applicative f => f (Doc ann) -> f (Doc ann) -> f (Doc ann)
 (<+>) = liftA2 (PP.<+>)
 
-(<>) :: Applicative f => f Doc -> f Doc -> f Doc
+(<>) :: Applicative f => f (Doc ann) -> f (Doc ann) -> f (Doc ann)
 (<>) = liftA2 (PP.<>)
 
-($+$) :: Applicative f => f Doc -> f Doc -> f Doc
-($+$) = liftA2 (PP.$+$)
+($+$) :: Applicative f => f (Doc ann) -> f (Doc ann) -> f (Doc ann)
+d1 $+$ d2 = f <$> d1 <*> d2
+ where
+  f x1 Empty = x1
+  f x1 x2 = PP.vcat [x1, x2]
 
-punctuate :: Applicative f => f Doc -> [f Doc] -> f [f Doc]
+punctuate :: Applicative f => f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
 punctuate p ds = map pure <$> (PP.punctuate <$> p <*> sequenceA ds)
 
-intercalate :: Monad f => f Doc -> [f Doc] -> f Doc
+intercalate :: Monad f => f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
 intercalate p ds = do
   ds' <- punctuate p ds
   hsep ds'
 
-bulletList :: Applicative f => f Doc -> [f Doc] -> f Doc
+bulletList :: Applicative f => f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
 bulletList bullet = vcat . map (hang bullet 2)
 
 ------------------------------------------------------------
 -- Running a pretty-printer
 
-renderDoc :: Sem (Reader PA ': r) Doc -> Sem r String
-renderDoc = fmap PP.render . runReader initPA
+renderDoc :: Sem (Reader PA ': r) (Doc ann) -> Sem r String
+renderDoc = fmap renderDoc' . runReader initPA
 
-renderDoc' :: Doc -> String
-renderDoc' = PP.render
+renderDoc' :: Doc ann -> String
+renderDoc' = renderString . PP.layoutPretty PP.defaultLayoutOptions
diff --git a/src/Disco/Property.hs b/src/Disco/Property.hs
index bdbd1092..c3edd902 100644
--- a/src/Disco/Property.hs
+++ b/src/Disco/Property.hs
@@ -79,7 +79,7 @@ generateSamples (Randomized n m) e
 -- Pretty-printing for test results
 ------------------------------------------------------------
 
-prettyResultCertainty :: Members '[LFresh, Reader PA] r => TestReason -> AProperty -> String -> Sem r Doc
+prettyResultCertainty :: Members '[LFresh, Reader PA] r => TestReason -> AProperty -> String -> Sem r (Doc ann)
 prettyResultCertainty r prop res =
   (if resultIsCertain r then "Certainly" else "Possibly") <+> text res <> ":" <+> pretty (eraseProperty prop)
 
@@ -88,11 +88,11 @@ prettyTestReason ::
   Bool ->
   AProperty ->
   TestReason ->
-  Sem r Doc
+  Sem r (Doc ann)
 prettyTestReason _ _ TestBool = empty
-prettyTestReason b prop (TestFound (TestResult _ tr env))
+prettyTestReason b _ (TestFound (TestResult _ _ env))
   | b = prettyTestEnv "Found example:" env
-  | not b = prettyTestReason b prop tr $+$ prettyTestEnv "Found counterexample:" env
+  | not b = prettyTestEnv "Found counterexample:" env
 prettyTestReason b _ (TestNotFound Exhaustive)
   | b = "No counterexamples exist; all possible values were checked."
   | not b = "No example exists; all possible values were checked."
@@ -112,16 +112,17 @@ prettyTestReason _ _ (TestLt t a1 a2) =
     , "Right side: " <> prettyValue t a2
     ]
 prettyTestReason _ _ (TestRuntimeError ee) =
-  "Test failed with an error:"
-    $+$ nest 2 (pretty (EvalErr ee))
+  nest 2 $
+    "Test failed with an error:"
+      $+$ pretty (EvalErr ee)
 -- \$+$
 -- prettyTestEnv "Example inputs that caused the error:" env
 -- See #364
 prettyTestReason b (ATApp _ (ATPrim _ (PrimBOp _)) (ATTup _ [p1, p2])) (TestBin _ tr1 tr2) =
   bulletList
     "-"
-    [ "Left side:" $+$ nest 2 (prettyTestResult' b p1 tr1)
-    , "Right side:" $+$ nest 2 (prettyTestResult' b p2 tr2)
+    [ nest 2 $ "Left side:" $+$ prettyTestResult' b p1 tr1
+    , nest 2 $ "Right side:" $+$ prettyTestResult' b p2 tr2
     ]
 -- See Note [prettyTestReason fallback]
 prettyTestReason _ _ _ = empty
@@ -151,7 +152,7 @@ prettyTestResult' ::
   Bool ->
   AProperty ->
   TestResult ->
-  Sem r Doc
+  Sem r (Doc ann)
 prettyTestResult' _ prop (TestResult bool tr _) =
   prettyResultCertainty tr prop (map toLower (show bool))
     $+$ prettyTestReason bool prop tr
@@ -160,16 +161,16 @@ prettyTestResult ::
   Members '[Input TyDefCtx, LFresh, Reader PA] r =>
   AProperty ->
   TestResult ->
-  Sem r Doc
+  Sem r (Doc ann)
 prettyTestResult prop (TestResult b r env) = prettyTestResult' b prop (TestResult b r env)
 
 prettyTestEnv ::
   Members '[Input TyDefCtx, LFresh, Reader PA] r =>
   String ->
   TestEnv ->
-  Sem r Doc
+  Sem r (Doc ann)
 prettyTestEnv _ (TestEnv []) = empty
-prettyTestEnv s (TestEnv vs) = text s $+$ nest 2 (vcat (map prettyBind vs))
+prettyTestEnv s (TestEnv vs) = nest 2 $ text s $+$ vcat (map prettyBind vs)
  where
   maxNameLen = maximum . map (\(n, _, _) -> length n) $ vs
   prettyBind (x, ty, v) =
diff --git a/src/Disco/Subst.hs b/src/Disco/Subst.hs
index 23e221cd..5d11c02a 100644
--- a/src/Disco/Subst.hs
+++ b/src/Disco/Subst.hs
@@ -72,7 +72,7 @@ instance Pretty a => Pretty (Substitution a) where
     ds <- punctuate "," es
     braces (hsep ds)
 
-prettyMapping :: (Pretty a, Members '[Reader PA, LFresh] r) => Name a -> a -> Sem r Doc
+prettyMapping :: (Pretty a, Members '[Reader PA, LFresh] r) => Name a -> a -> Sem r (Doc ann)
 prettyMapping x a = pretty x <+> "->" <+> pretty a
 
 -- | The domain of a substitution is the set of names for which the
diff --git a/src/Disco/Typecheck.hs b/src/Disco/Typecheck.hs
index a67f25c4..a2ff9b0d 100644
--- a/src/Disco/Typecheck.hs
+++ b/src/Disco/Typecheck.hs
@@ -114,7 +114,7 @@ inferTelescope inferOne tel = do
 --   imports should already be checked and passed in as the second
 --   argument.
 checkModule ::
-  Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r =>
+  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r =>
   ModuleName ->
   Map ModuleName ModuleInfo ->
   Module ->
@@ -268,7 +268,7 @@ checkCtx = mapM_ checkPolyTyValid . Ctx.elems
 
 -- | Type check a top-level definition in the given module.
 checkDefn ::
-  Members '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh, Output Message] r =>
+  Members '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh, Output (Message ann)] r =>
   ModuleName ->
   TermDefn ->
   Sem r Defn
@@ -336,7 +336,7 @@ checkDefn name (TermDefn x clauses) = mapError (LocTCError (Just (name .- x))) $
 -- | Given a context mapping names to documentation, extract the
 --   properties attached to each name and typecheck them.
 checkProperties ::
-  Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output Message] r =>
+  Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r =>
   Ctx Term Docs ->
   Sem r (Ctx ATerm [AProperty])
 checkProperties docs =
@@ -348,7 +348,7 @@ checkProperties docs =
 
 -- | Check the types of the terms embedded in a property.
 checkProperty ::
-  Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output Message] r =>
+  Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r =>
   Property ->
   Sem r AProperty
 checkProperty prop = do
@@ -445,7 +445,7 @@ infer = typecheck Infer
 --   for a term by running type inference, solving the resulting
 --   constraints, and quantifying over any remaining type variables.
 inferTop ::
-  Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
+  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
   Term ->
   Sem r (ATerm, PolyType)
 inferTop t = do
@@ -473,7 +473,7 @@ inferTop t = do
 --   polymorphic type by running type checking and solving the
 --   resulting constraints.
 checkTop ::
-  Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
+  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
   Term ->
   PolyType ->
   Sem r ATerm
diff --git a/src/Disco/Typecheck/Solve.hs b/src/Disco/Typecheck/Solve.hs
index 5de75a3e..5d00e431 100644
--- a/src/Disco/Typecheck/Solve.hs
+++ b/src/Disco/Typecheck/Solve.hs
@@ -249,7 +249,7 @@ lkup messg m k = fromMaybe (error errMsg) (M.lookup k m)
 -- Top-level solver algorithm
 
 solveConstraint ::
-  Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r =>
+  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
   Constraint ->
   Sem r S
 solveConstraint c = do
@@ -271,7 +271,7 @@ solveConstraint c = do
   asum' (map (uncurry solveConstraintChoice) qcList)
 
 solveConstraintChoice ::
-  Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r =>
+  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
   TyVarInfoMap ->
   [SimpleConstraint] ->
   Sem r S
@@ -487,7 +487,7 @@ checkQual q (ABase bty) =
 --   constraints, that is, only of the form (v1 <: v2), (v <: b), or
 --   (b <: v), where v is a type variable and b is a base type.
 simplify ::
-  Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
+  Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
   TyVarInfoMap ->
   [SimpleConstraint] ->
   Sem r (TyVarInfoMap, [(Atom, Atom)], S)
@@ -517,7 +517,7 @@ simplify origVM cs =
   -- Iterate picking one simplifiable constraint and simplifying it
   -- until none are left.
   simplify' ::
-    Members '[State SimplifyState, Fresh, Error SolveError, Output Message, Input TyDefCtx] r =>
+    Members '[State SimplifyState, Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
     Sem r ()
   simplify' = do
     -- q <- gets fst
@@ -751,7 +751,7 @@ mkConstraintGraph as cs = G.mkGraph nodes (S.fromList cs)
 --   only unsorted variables, just unify them all with the skolem and
 --   remove those components.
 checkSkolems ::
-  Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
+  Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
   TyVarInfoMap ->
   Graph Atom ->
   Sem r (Graph UAtom, S)
@@ -784,7 +784,7 @@ checkSkolems vm graph = do
   noSkolems (AVar (S v)) = error $ "Skolem " ++ show v ++ " remaining in noSkolems"
 
   unifyWCCs ::
-    Members '[Error SolveError, Output Message, Input TyDefCtx] r =>
+    Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r =>
     Graph Atom ->
     S ->
     [Set Atom] ->
@@ -964,7 +964,7 @@ glbBySort vm rm = limBySort vm rm SubTy
 --   predecessors in this case, since it seems nice to default to
 --   "simpler" types lower down in the subtyping chain.
 solveGraph ::
-  Members '[Fresh, Error SolveError, Output Message] r =>
+  Members '[Fresh, Error SolveError, Output (Message ann)] r =>
   TyVarInfoMap ->
   Graph UAtom ->
   Sem r S
@@ -1030,7 +1030,7 @@ solveGraph vm g = atomToTypeSubst . unifyWCC <$> go topRelMap
     fromVar _ = error "Impossible! UB but uisVar."
 
   go ::
-    Members '[Fresh, Error SolveError, Output Message] r =>
+    Members '[Fresh, Error SolveError, Output (Message ann)] r =>
     RelMap ->
     Sem r (Substitution BaseTy)
   go relMap@(RelMap rm) =
diff --git a/src/Disco/Typecheck/Util.hs b/src/Disco/Typecheck/Util.hs
index 1c70dfa0..258d6b9f 100644
--- a/src/Disco/Typecheck/Util.hs
+++ b/src/Disco/Typecheck/Util.hs
@@ -1,6 +1,3 @@
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
 
 -- |
 -- Module      :  Disco.Typecheck.Util
@@ -148,7 +145,7 @@ withConstraint = fmap swap . runWriter
 --   the resulting substitution (or failing with an error).  Note that
 --   this locally dispatches the constraint writer effect.
 solve ::
-  Members '[Reader TyDefCtx, Error TCError, Output Message] r =>
+  Members '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
   Sem (Writer Constraint ': r) a ->
   Sem r (a, S)
 solve m = do
diff --git a/src/Disco/Value.hs b/src/Disco/Value.hs
index 21893e02..e8358117 100644
--- a/src/Disco/Value.hs
+++ b/src/Disco/Value.hs
@@ -460,10 +460,10 @@ set n c = modify $ \(Mem nxt m) -> Mem nxt (IM.insert n c m)
 -- Pretty-printing values
 ------------------------------------------------------------
 
-prettyValue' :: Member (Input TyDefCtx) r => Type -> Value -> Sem r Doc
+prettyValue' :: Member (Input TyDefCtx) r => Type -> Value -> Sem r (Doc ann)
 prettyValue' ty v = runLFresh . runReader initPA $ prettyValue ty v
 
-prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc
+prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann)
 -- Lazily expand any user-defined types
 prettyValue (TyUser x args) v = do
   tydefs <- input
@@ -520,23 +520,23 @@ prettyValue ty@TyCon {} v =
 
 -- | Pretty-print a value with guaranteed parentheses.  Do nothing for
 --   tuples; add an extra set of parens for other values.
-prettyVP :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc
+prettyVP :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann)
 prettyVP ty@(_ :*: _) = prettyValue ty
 prettyVP ty = parens . prettyValue ty
 
-prettyPlaceholder :: Members '[Reader PA, LFresh] r => Type -> Sem r Doc
+prettyPlaceholder :: Members '[Reader PA, LFresh] r => Type -> Sem r (Doc ann)
 prettyPlaceholder ty = "<" <> pretty ty <> ">"
 
-prettyTuple :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc
+prettyTuple :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann)
 prettyTuple (ty1 :*: ty2) (VPair v1 v2) = prettyValue ty1 v1 <> "," <+> prettyTuple ty2 v2
 prettyTuple ty v = prettyValue ty v
 
 -- | 'prettySequence' pretty-prints a lists of values separated by a delimiter.
-prettySequence :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Doc -> [Value] -> Sem r Doc
+prettySequence :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Doc ann -> [Value] -> Sem r (Doc ann)
 prettySequence ty del vs = hsep =<< punctuate (return del) (map (prettyValue ty) vs)
 
 -- | Pretty-print a literal bag value.
-prettyBag :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> [(Value, Integer)] -> Sem r Doc
+prettyBag :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> [(Value, Integer)] -> Sem r (Doc ann)
 prettyBag _ [] = bag empty
 prettyBag ty vs
   | all ((== 1) . snd) vs = bag $ prettySequence ty "," (map fst vs)
diff --git a/test/compile-misc/expected b/test/compile-misc/expected
index 4cd50107..eafae62e 100644
--- a/test/compile-misc/expected
+++ b/test/compile-misc/expected
@@ -2,8 +2,8 @@ holds (∀ℕ. (λarg0. (λ_. (λk. (λx. test [(x, ℕ, x)] (3 < x)) arg0) (λ_
 λx, y. x
 (λ_. (λk. (λy. (λp, q. p) (fst y) (snd y)) (frac (2 / 3))) (λ_1. matchErr)) unit
 (λ_. (λk. case (3 < 2) of {
-            left _1 -> k unit
-            right px -> (λ_2. 1) px
-          }) (λ_1. (λk. 17) (λ_2. matchErr))) unit
+  left _1 -> k unit
+  right px -> (λ_2. 1) px
+  }) (λ_1. (λk. 17) (λ_2. matchErr))) unit
 (10 choose right (5, left unit))
 5!
diff --git a/test/repl-proptest/expected b/test/repl-proptest/expected
index 4fcdf0a7..52a7b04e 100644
--- a/test/repl-proptest/expected
+++ b/test/repl-proptest/expected
@@ -7,8 +7,6 @@
       a = false
       b = false
   - Certainly false: ∀a, b. (a /\ b) =!= (a \/ b)
-    - Left side:  false
-    - Right side: true
     Found counterexample:
       a = false
       b = true
diff --git a/test/types-char-string/expected b/test/types-char-string/expected
index 62bf6a20..c8da8ccd 100644
--- a/test/types-char-string/expected
+++ b/test/types-char-string/expected
@@ -12,7 +12,7 @@ true
 2
 3
 (λx. {? 1 when x is 'a' 
-     ?})("Disco")
+?})("Disco")
 1:3:
   |
 1 | ' a'