diff --git a/what4-abc/src/What4/Solver/ABC.hs b/what4-abc/src/What4/Solver/ABC.hs
index 7057799a..22adb9f9 100644
--- a/what4-abc/src/What4/Solver/ABC.hs
+++ b/what4-abc/src/What4/Solver/ABC.hs
@@ -70,11 +70,11 @@ import qualified Data.Set as Set
 import qualified Data.Text as T
 import           Foreign.C.Types
 import           Numeric.Natural
+import           Prettyprinter
 import           System.Directory
 import           System.IO
 import qualified System.IO.Streams as Streams
 import           System.Process
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import           What4.BaseTypes
 import           What4.Concrete
@@ -108,7 +108,7 @@ abcQbfIterations = configOption BaseIntegerRepr "abc.qbf_max_iterations"
 abcOptions :: [ConfigDesc]
 abcOptions =
   [ opt abcQbfIterations (ConcreteInteger (toInteger (maxBound :: CInt)))
-    (text "Max number of iterations to run ABC's QBF solver")
+    ("Max number of iterations to run ABC's QBF solver" :: T.Text)
   ]
 
 abcAdapter :: SolverAdapter st
@@ -132,7 +132,7 @@ satCommand = configOption knownRepr "sat_command"
 genericSatOptions :: [ConfigDesc]
 genericSatOptions =
   [ opt satCommand (ConcreteString "glucose $1")
-    (text "Generic SAT solving command to run")
+    ("Generic SAT solving command to run" :: T.Text)
   ]
 
 genericSatAdapter :: SolverAdapter st
@@ -249,16 +249,20 @@ eval' ntk e = do
 
 failAt :: ProgramLoc -> String -> IO a
 failAt l msg = fail $ show $
-   text msg <$$>
-   text "From term created at" <+> pretty (plSourceLoc l)
+  vcat
+  [ text msg
+  , text "From term created at" <+> pretty (plSourceLoc l)
+  ]
 
 failTerm :: Expr t tp -> String -> IO a
 failTerm e nm = do
   fail $ show $
-    text "The" <+> text nm <+> text "created at"
+    vcat
+    [ text "The" <+> text nm <+> text "created at"
          <+> pretty (plSourceLoc (exprLoc e))
-         <+> text "is not supported by ABC:" <$$>
-    indent 2 (ppExpr e)
+         <+> text "is not supported by ABC:"
+    , indent 2 (ppExpr e)
+    ]
 
 bitblastPred :: Network t s -> NonceAppExpr t tp -> IO (NameType s tp)
 bitblastPred h e = do
@@ -731,8 +735,10 @@ checkSupportedByAbc vars = do
   let errors = Fold.toList (vars^.varErrors)
   -- Check no errors where reported in result.
   when (not (null errors)) $ do
-    fail $ show $ text "This formula is not supported by abc:" <$$>
-                  indent 2 (vcat errors)
+    fail $ show $ vcat
+      [ text "This formula is not supported by abc:"
+      , indent 2 (vcat errors)
+      ]
 
 checkNoLatches :: MonadFail m => CollectedVarInfo t -> m ()
 checkNoLatches vars = do
@@ -1039,3 +1045,6 @@ getInputCount ntk = GIA.inputCount (gia ntk)
 -- | Return number of outputs so far in network.
 getOutputCount :: Network t s -> IO Int
 getOutputCount ntk = length <$> readIORef (revOutputs ntk)
+
+text :: String -> Doc ann
+text = pretty
diff --git a/what4-abc/what4-abc.cabal b/what4-abc/what4-abc.cabal
index c0f4f55b..a0099a6e 100644
--- a/what4-abc/what4-abc.cabal
+++ b/what4-abc/what4-abc.cabal
@@ -20,7 +20,6 @@ library
     base >= 4.7 && < 4.15,
     aig,
     abcBridge >= 0.11,
-    ansi-wl-pprint,
     bv-sized >= 1.0.0,
     containers,
     what4 >= 0.4,
@@ -29,6 +28,7 @@ library
     lens,
     mtl,
     parameterized-utils,
+    prettyprinter >= 1.7.0,
     process,
     text,
     transformers,
diff --git a/what4-blt/src/What4/Solver/BLT.hs b/what4-blt/src/What4/Solver/BLT.hs
index b8e6bc86..08e7bf3e 100644
--- a/what4-blt/src/What4/Solver/BLT.hs
+++ b/what4-blt/src/What4/Solver/BLT.hs
@@ -77,7 +77,7 @@ import qualified Data.Text as T
 import           Data.Traversable
 import           Data.Typeable
 import           System.IO (hPutStrLn, stderr)
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import           Prettyprinter
 
 import qualified Data.Parameterized.HashTable as PH
 import           Data.Parameterized.Nonce
@@ -106,7 +106,7 @@ bltParams = configOption knownRepr "blt_params"
 bltOptions :: [ConfigDesc]
 bltOptions =
   [ opt         bltParams         (ConcreteString (UnicodeLiteral ""))
-    (text "Command-line parameters to send to BLT")
+    ("Command-line parameters to send to BLT" :: T.Text)
   ]
 
 bltAdapter :: SolverAdapter t
@@ -415,8 +415,10 @@ assume h (NonceAppExpr (nonceExprApp -> Annotation _ _ x)) =
   assume h x
 assume _ (NonceAppExpr e) =
   fail . show $
-    text "Unsupported term created at" <+> pretty (plSourceLoc l) <>
-    text ":" <$$> indent 2 (pretty (NonceAppExpr e))
+  vcat
+  [ "Unsupported term created at" <+> pretty (plSourceLoc l) <> ":"
+  , indent 2 (pretty (NonceAppExpr e))
+  ]
   where
   l = nonceExprLoc e
 assume h (BoolExpr b l)
@@ -447,9 +449,11 @@ assume h b@(AppExpr ba) =
         appLEq x' y'
       _ -> unsupported
   where
-  unsupported = fail $ show $
-        text "Unsupported term created at" <+> pretty (plSourceLoc l) <>
-        text ":" <$$> indent 2 (pretty b)
+  unsupported =
+    fail $ show $ vcat
+    [ "Unsupported term created at" <+> pretty (plSourceLoc l) <> ":"
+    , indent 2 (pretty b)
+    ]
   l = appExprLoc ba
   appLEq lhs rhs =
     let (lhs', rhs') = normalizeLEQ lhs rhs in
diff --git a/what4-blt/what4-blt.cabal b/what4-blt/what4-blt.cabal
index 55ccddc5..4abcb057 100644
--- a/what4-blt/what4-blt.cabal
+++ b/what4-blt/what4-blt.cabal
@@ -18,12 +18,12 @@ Description:
 library
   build-depends:
     base >= 4.7 && < 4.15,
-    ansi-wl-pprint,
     blt >= 0.12.1,
     containers,
     what4 >= 0.4,
     lens >= 1.2,
     parameterized-utils,
+    prettyprinter >= 1.7.0,
     text,
     transformers
 
diff --git a/what4/src/What4/BaseTypes.hs b/what4/src/What4/BaseTypes.hs
index 029c5f82..2ba07adb 100644
--- a/what4/src/What4/BaseTypes.hs
+++ b/what4/src/What4/BaseTypes.hs
@@ -84,7 +84,7 @@ import qualified Data.Parameterized.Context as Ctx
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.TH.GADT
 import           GHC.TypeNats as TypeNats
-import           Text.PrettyPrint.ANSI.Leijen
+import           Prettyprinter
 
 --------------------------------------------------------------------------------
 -- KnownCtx
@@ -290,19 +290,19 @@ instance Hashable (StringInfoRepr si) where
   hashWithSalt = $(structuralHashWithSalt [t|StringInfoRepr|] [])
 
 instance Pretty (BaseTypeRepr bt) where
-  pretty = text . show
+  pretty = pretty . show
 instance Show (BaseTypeRepr bt) where
   showsPrec = $(structuralShowsPrec [t|BaseTypeRepr|])
 instance ShowF BaseTypeRepr
 
 instance Pretty (FloatPrecisionRepr fpp) where
-  pretty = text . show
+  pretty = pretty . show
 instance Show (FloatPrecisionRepr fpp) where
   showsPrec = $(structuralShowsPrec [t|FloatPrecisionRepr|])
 instance ShowF FloatPrecisionRepr
 
 instance Pretty (StringInfoRepr si) where
-  pretty = text . show
+  pretty = pretty . show
 instance Show (StringInfoRepr si) where
   showsPrec = $(structuralShowsPrec [t|StringInfoRepr|])
 instance ShowF StringInfoRepr
diff --git a/what4/src/What4/Concrete.hs b/what4/src/What4/Concrete.hs
index 03eb6d74..cad4c8c7 100644
--- a/what4/src/What4/Concrete.hs
+++ b/what4/src/What4/Concrete.hs
@@ -52,7 +52,7 @@ import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import qualified Numeric as N
 import           Numeric.Natural
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 import qualified Data.BitVector.Sized as BV
 import           Data.Parameterized.Classes
@@ -148,26 +148,30 @@ instance OrdF ConcreteVal where
 instance Ord (ConcreteVal tp) where
   compare x y = toOrdering (compareF x y)
 
+-- | Pretty-print a rational number.
+ppRational :: Rational -> PP.Doc ann
+ppRational x = PP.pretty (show x)
+
 -- | Pretty-print a concrete value
-ppConcrete :: ConcreteVal tp -> PP.Doc
+ppConcrete :: ConcreteVal tp -> PP.Doc ann
 ppConcrete = \case
-  ConcreteBool x -> PP.text (show x)
-  ConcreteNat x -> PP.text (show x)
-  ConcreteInteger x -> PP.text (show x)
-  ConcreteReal x -> PP.text (show x)
-  ConcreteString x -> PP.text (show x)
-  ConcreteBV w x -> PP.text ("0x" ++ (N.showHex (BV.asUnsigned x) (":[" ++ show w ++ "]")))
-  ConcreteComplex (r :+ i) -> PP.text "complex(" PP.<> PP.text (show r) PP.<> PP.text ", " PP.<> PP.text (show i) PP.<> PP.text ")"
-  ConcreteStruct xs -> PP.text "struct(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete xs)) PP.<> PP.text ")"
-  ConcreteArray _ def xs0 -> go (Map.toAscList xs0) (PP.text "constArray(" PP.<> ppConcrete def PP.<> PP.text ")")
+  ConcreteBool x -> PP.pretty x
+  ConcreteNat x -> PP.pretty x
+  ConcreteInteger x -> PP.pretty x
+  ConcreteReal x -> ppRational x
+  ConcreteString x -> PP.pretty (show x)
+  ConcreteBV w x -> PP.pretty ("0x" ++ (N.showHex (BV.asUnsigned x) (":[" ++ show w ++ "]")))
+  ConcreteComplex (r :+ i) -> PP.pretty "complex(" PP.<> ppRational r PP.<> PP.pretty ", " PP.<> ppRational i PP.<> PP.pretty ")"
+  ConcreteStruct xs -> PP.pretty "struct(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete xs)) PP.<> PP.pretty ")"
+  ConcreteArray _ def xs0 -> go (Map.toAscList xs0) (PP.pretty "constArray(" PP.<> ppConcrete def PP.<> PP.pretty ")")
     where
     go  [] doc = doc
     go ((i,x):xs) doc = ppUpd i x (go xs doc)
 
     ppUpd i x doc =
-       PP.text "update(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete i))
+       PP.pretty "update(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete i))
                          PP.<> PP.comma
                          PP.<> ppConcrete x
                          PP.<> PP.comma
                          PP.<> doc
-                         PP.<> PP.text ")"
+                         PP.<> PP.pretty ")"
diff --git a/what4/src/What4/Config.hs b/what4/src/What4/Config.hs
index e088b9f8..24160793 100644
--- a/what4/src/What4/Config.hs
+++ b/what4/src/What4/Config.hs
@@ -176,7 +176,7 @@ import           Numeric.Natural
 import           System.IO ( Handle, hPutStr )
 import           System.IO.Error ( ioeGetErrorString )
 
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
+import           Prettyprinter hiding (Unbounded)
 
 import           What4.BaseTypes
 import           What4.Concrete
@@ -253,8 +253,8 @@ configOptionType (ConfigOption tp _) = tp
 --   attempting to alter the option setting.
 data OptionSetResult =
   OptionSetResult
-  { optionSetError    :: !(Maybe Doc)
-  , optionSetWarnings :: !(Seq Doc)
+  { optionSetError    :: !(Maybe (Doc ()))
+  , optionSetWarnings :: !(Seq (Doc ()))
   }
 
 instance Semigroup OptionSetResult where
@@ -272,11 +272,11 @@ optOK :: OptionSetResult
 optOK = OptionSetResult{ optionSetError = Nothing, optionSetWarnings = mempty }
 
 -- | Reject the new option value with an error message.
-optErr :: Doc -> OptionSetResult
+optErr :: Doc () -> OptionSetResult
 optErr x = OptionSetResult{ optionSetError = Just x, optionSetWarnings = mempty }
 
 -- | Accept the given option value, but report a warning message.
-optWarn :: Doc -> OptionSetResult
+optWarn :: Doc () -> OptionSetResult
 optWarn x = OptionSetResult{ optionSetError = Nothing, optionSetWarnings = Seq.singleton x }
 
 
@@ -312,7 +312,7 @@ data OptionStyle (tp :: BaseType) =
     -- If the validation fails, the operation should return a result
     -- describing why validation failed. Optionally, warnings may also be returned.
 
-  , opt_help :: Doc
+  , opt_help :: Doc ()
     -- ^ Documentation for the option to be displayed in the event a user asks for information
     --   about this option.  This message should contain information relevant to all options in this
     --   style (e.g., its type and range of expected values), not necessarily
@@ -330,7 +330,7 @@ defaultOpt tp =
   OptionStyle
   { opt_type = tp
   , opt_onset = \_ _ -> return mempty
-  , opt_help = empty
+  , opt_help = mempty
   , opt_default_value = Nothing
   }
 
@@ -341,7 +341,7 @@ set_opt_onset :: (Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult
 set_opt_onset f s = s { opt_onset = f }
 
 -- | Update the @opt_help@ field.
-set_opt_help :: Doc
+set_opt_help :: Doc ()
              -> OptionStyle tp
              -> OptionStyle tp
 set_opt_help v s = s { opt_help = v }
@@ -395,7 +395,7 @@ checkBound lo hi a = checkLo lo a && checkHi a hi
        checkHi x (Inclusive y) = x <= y
        checkHi x (Exclusive y) = x <  y
 
-docInterval :: Show a => Bound a -> Bound a -> Doc
+docInterval :: Show a => Bound a -> Bound a -> Doc ann
 docInterval lo hi = docLo lo <> text ", " <> docHi hi
  where docLo Unbounded      = text "(-∞"
        docLo (Exclusive r)  = text "(" <> text (show r)
@@ -450,7 +450,7 @@ integerWithMaxOptSty hi = integerWithRangeOptSty Unbounded hi
 enumOptSty :: Set Text -> OptionStyle (BaseStringType Unicode)
 enumOptSty elts = stringOptSty & set_opt_onset vf
                                & set_opt_help help
-  where help = group (text "one of: " <+> align (sep $ map (dquotes . text . Text.unpack) $ Set.toList elts))
+  where help = group (text "one of: " <+> align (sep $ map (dquotes . pretty) $ Set.toList elts))
         vf :: Maybe (ConcreteVal (BaseStringType Unicode))
            -> ConcreteVal (BaseStringType Unicode)
            -> IO OptionSetResult
@@ -459,7 +459,7 @@ enumOptSty elts = stringOptSty & set_opt_onset vf
          | otherwise = return $ optErr $
                             text "invalid setting" <+> text (show x) <+>
                             text ", expected one of:" <+>
-                            align (sep (map (text . Text.unpack) $ Set.toList elts))
+                            align (sep (map pretty $ Set.toList elts))
 
 -- | A configuration syle for options that must be one of a fixed set of text values.
 --   Associated with each string is a validation/callback action that will be run
@@ -469,7 +469,7 @@ listOptSty
   -> OptionStyle (BaseStringType Unicode)
 listOptSty values =  stringOptSty & set_opt_onset vf
                                   & set_opt_help help
-  where help = group (text "one of: " <+> align (sep $ map (dquotes . text . Text.unpack . fst) $ Map.toList values))
+  where help = group (text "one of: " <+> align (sep $ map (dquotes . pretty . fst) $ Map.toList values))
         vf :: Maybe (ConcreteVal (BaseStringType Unicode))
            -> ConcreteVal (BaseStringType Unicode)
            -> IO OptionSetResult
@@ -478,7 +478,7 @@ listOptSty values =  stringOptSty & set_opt_onset vf
           (return $ optErr $
             text "invalid setting" <+> text (show x) <+>
             text ", expected one of:" <+>
-            align (sep (map (text . Text.unpack . fst) $ Map.toList values)))
+            align (sep (map (pretty . fst) $ Map.toList values)))
           (Map.lookup x values)
 
 
@@ -505,12 +505,12 @@ executablePathOptSty = stringOptSty & set_opt_onset vf
 --   an @OptionStyle@ describing the sort of option it is, and an optional
 --   help message describing the semantics of this option.
 data ConfigDesc where
-  ConfigDesc :: ConfigOption tp -> OptionStyle tp -> Maybe Doc -> ConfigDesc
+  ConfigDesc :: ConfigOption tp -> OptionStyle tp -> Maybe (Doc ()) -> ConfigDesc
 
 -- | The most general method for construcing a normal `ConfigDesc`.
 mkOpt :: ConfigOption tp     -- ^ Fixes the name and the type of this option
       -> OptionStyle tp      -- ^ Define the style of this option
-      -> Maybe Doc           -- ^ Help text
+      -> Maybe (Doc ())      -- ^ Help text
       -> Maybe (ConcreteVal tp) -- ^ A default value for this option
       -> ConfigDesc
 mkOpt o sty h def = ConfigDesc o sty{ opt_default_value = def } h
@@ -577,7 +577,7 @@ data ConfigLeaf where
   ConfigLeaf ::
     !(OptionStyle tp)              {- Style for this option -} ->
     IORef (Maybe (ConcreteVal tp)) {- State of the option -} ->
-    Maybe Doc                      {- Help text for the option -} ->
+    Maybe (Doc ())                 {- Help text for the option -} ->
     ConfigLeaf
 
 -- | Main configuration data type.  It is organized as a trie based on the
@@ -689,7 +689,7 @@ builtInOpts :: Integer -> [ConfigDesc]
 builtInOpts initialVerbosity =
   [ opt verbosity
         (ConcreteInteger initialVerbosity)
-        (text "Verbosity of the simulator: higher values produce more detailed informational and debugging output.")
+        ("Verbosity of the simulator: higher values produce more detailed informational and debugging output." :: Text)
   ]
 
 -- | Return an operation that will consult the current value of the
@@ -715,7 +715,7 @@ class Opt (tp :: BaseType) (a :: Type) | tp -> a where
 
   -- | Set the value of an option.  Return any generated warnings.
   --   Throw an exception if a validation error occurs.
-  setOpt :: OptionSetting tp -> a -> IO [Doc]
+  setOpt :: OptionSetting tp -> a -> IO [Doc ()]
   setOpt x v = trySetOpt x v >>= checkOptSetResult
 
   -- | Get the current value of an option.  Throw an exception
@@ -726,7 +726,7 @@ class Opt (tp :: BaseType) (a :: Type) | tp -> a where
 
 -- | Throw an exception if the given @OptionSetResult@ indidcates
 --   an error.  Otherwise, return any generated warnings.
-checkOptSetResult :: OptionSetResult -> IO [Doc]
+checkOptSetResult :: OptionSetResult -> IO [Doc ()]
 checkOptSetResult res =
   case optionSetError res of
     Just msg -> fail (show msg)
@@ -830,16 +830,19 @@ getConfigValues prefix (Config cfg) =
      toList <$> execWriterT (traverseSubtree ps f m)
 
 
-ppSetting :: [Text] -> Maybe (ConcreteVal tp) -> Doc
-ppSetting nm v = fill 30 (text (Text.unpack (Text.intercalate "." nm))
-                           <> maybe empty (\x -> text " = " <> ppConcrete x) v
+ppSetting :: [Text] -> Maybe (ConcreteVal tp) -> Doc ann
+ppSetting nm v = fill 30 (pretty (Text.intercalate "." nm)
+                           <> maybe mempty (\x -> text " = " <> ppConcrete x) v
                          )
 
-ppOption :: [Text] -> OptionStyle tp -> Maybe (ConcreteVal tp) -> Maybe Doc -> Doc
+ppOption :: [Text] -> OptionStyle tp -> Maybe (ConcreteVal tp) -> Maybe (Doc ()) -> Doc ()
 ppOption nm sty x help =
-   group (ppSetting nm x <//> indent 2 (opt_help sty)) <$$> maybe empty (indent 2) help
+  vcat
+  [ group $ fillCat [ppSetting nm x, indent 2 (opt_help sty)]
+  , maybe mempty (indent 2) help
+  ]
 
-ppConfigLeaf :: [Text] -> ConfigLeaf -> IO Doc
+ppConfigLeaf :: [Text] -> ConfigLeaf -> IO (Doc ())
 ppConfigLeaf nm (ConfigLeaf sty ref help) =
   do x <- readIORef ref
      return $ ppOption nm sty x help
@@ -851,12 +854,15 @@ ppConfigLeaf nm (ConfigLeaf sty ref help) =
 configHelp ::
   Text ->
   Config ->
-  IO [Doc]
+  IO [Doc ()]
 configHelp prefix (Config cfg) =
   do m <- readIORef cfg
      let ps = Text.splitOn "." prefix
-         f :: [Text] -> ConfigLeaf -> WriterT (Seq Doc) IO ConfigLeaf
+         f :: [Text] -> ConfigLeaf -> WriterT (Seq (Doc ())) IO ConfigLeaf
          f nm leaf = do d <- liftIO (ppConfigLeaf nm leaf)
                         tell (Seq.singleton d)
                         return leaf
      toList <$> (execWriterT (traverseSubtree ps f m))
+
+text :: String -> Doc ann
+text = pretty
diff --git a/what4/src/What4/Expr/App.hs b/what4/src/What4/Expr/App.hs
index 70aad22b..7149873d 100644
--- a/what4/src/What4/Expr/App.hs
+++ b/what4/src/What4/Expr/App.hs
@@ -55,7 +55,7 @@ import           Data.Ratio (numerator, denominator)
 import           Data.Text (Text)
 import qualified Data.Text as Text
 import           Numeric.Natural
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import           Prettyprinter hiding (Unbounded)
 
 import           What4.BaseTypes
 import           What4.Interface
@@ -1380,12 +1380,12 @@ ppNonceApp ppFn a0 = do
       where resolve f_nm = prettyApp "apply" (f_nm : toListFC exprPrettyArg a)
 
 instance ShowF e => Pretty (App e u) where
-  pretty a = text (Text.unpack nm) <+> sep (ppArg <$> args)
+  pretty a = pretty nm <+> sep (ppArg <$> args)
     where (nm, args) = ppApp' a
-          ppArg :: PrettyArg e -> Doc
-          ppArg (PrettyArg e) = text (showF e)
-          ppArg (PrettyText txt) = text (Text.unpack txt)
-          ppArg (PrettyFunc fnm fargs) = parens (text (Text.unpack fnm) <+> sep (ppArg <$> fargs))
+          ppArg :: PrettyArg e -> Doc ann
+          ppArg (PrettyArg e) = pretty (showF e)
+          ppArg (PrettyText txt) = pretty txt
+          ppArg (PrettyFunc fnm fargs) = parens (pretty fnm <+> sep (ppArg <$> fargs))
 
 instance ShowF e => Show (App e u) where
   show = show . pretty
diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
index 8d39a68d..0e88d8ea 100644
--- a/what4/src/What4/Expr/Builder.hs
+++ b/what4/src/What4/Expr/Builder.hs
@@ -208,8 +208,7 @@ import qualified Data.Text as Text
 import           Data.Word (Word64)
 import           GHC.Generics (Generic)
 import           Numeric.Natural
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import           Prettyprinter hiding (Unbounded)
 
 import           What4.BaseTypes
 import           What4.Concrete
@@ -868,44 +867,44 @@ instance Pretty (Expr t tp) where
 
 
 -- | @AppPPExpr@ represents a an application, and it may be let bound.
-data AppPPExpr
+data AppPPExpr ann
    = APE { apeIndex :: !PPIndex
          , apeLoc :: !ProgramLoc
          , apeName :: !Text
-         , apeExprs :: ![PPExpr]
+         , apeExprs :: ![PPExpr ann]
          , apeLength :: !Int
            -- ^ Length of AppPPExpr not including parenthesis.
          }
 
-data PPExpr
-   = FixedPPExpr !Doc ![Doc] !Int
+data PPExpr ann
+   = FixedPPExpr !(Doc ann) ![Doc ann] !Int
      -- ^ A fixed doc with length.
-   | AppPPExpr !AppPPExpr
+   | AppPPExpr !(AppPPExpr ann)
      -- ^ A doc that can be let bound.
 
 -- | Pretty print a AppPPExpr
-apeDoc :: AppPPExpr -> (Doc, [Doc])
-apeDoc a = (text (Text.unpack (apeName a)), ppExprDoc True <$> apeExprs a)
+apeDoc :: AppPPExpr ann -> (Doc ann, [Doc ann])
+apeDoc a = (pretty (apeName a), ppExprDoc True <$> apeExprs a)
 
-textPPExpr :: Text -> PPExpr
-textPPExpr t = FixedPPExpr (text (Text.unpack t)) [] (Text.length t)
+textPPExpr :: Text -> PPExpr ann
+textPPExpr t = FixedPPExpr (pretty t) [] (Text.length t)
 
-stringPPExpr :: String -> PPExpr
-stringPPExpr t = FixedPPExpr (text t) [] (length t)
+stringPPExpr :: String -> PPExpr ann
+stringPPExpr t = FixedPPExpr (pretty t) [] (length t)
 
 -- | Get length of Expr including parens.
-ppExprLength :: PPExpr -> Int
+ppExprLength :: PPExpr ann -> Int
 ppExprLength (FixedPPExpr _ [] n) = n
 ppExprLength (FixedPPExpr _ _ n) = n + 2
 ppExprLength (AppPPExpr a) = apeLength a + 2
 
-parenIf :: Bool -> Doc -> [Doc] -> Doc
+parenIf :: Bool -> Doc ann -> [Doc ann] -> Doc ann
 parenIf _ h [] = h
 parenIf False h l = hsep (h:l)
 parenIf True h l = parens (hsep (h:l))
 
 -- | Pretty print PPExpr
-ppExprDoc :: Bool -> PPExpr -> Doc
+ppExprDoc :: Bool -> PPExpr ann -> Doc ann
 ppExprDoc b (FixedPPExpr d a _) = parenIf b d a
 ppExprDoc b (AppPPExpr a) = uncurry (parenIf b) (apeDoc a)
 
@@ -920,28 +919,29 @@ defaultPPExprOpts =
             }
 
 -- | Pretty print an 'Expr' using let bindings to create the term.
-ppExpr :: Expr t tp -> Doc
+ppExpr :: Expr t tp -> Doc ann
 ppExpr e
      | Prelude.null bindings = ppExprDoc False r
      | otherwise =
-         text "let" <+> align (vcat bindings) PP.<$>
-         text " in" <+> align (ppExprDoc False r)
+       vsep
+       [ text "let" <+> align (vcat bindings)
+       , text " in" <+> align (ppExprDoc False r) ]
   where (bindings,r) = runST (ppExpr' e defaultPPExprOpts)
 
 instance ShowF (Expr t)
 
 -- | Pretty print the top part of an element.
-ppExprTop :: Expr t tp -> Doc
+ppExprTop :: Expr t tp -> Doc ann
 ppExprTop e = ppExprDoc False r
   where (_,r) = runST (ppExpr' e defaultPPExprOpts)
 
 -- | Contains the elements before, the index, doc, and width and
 -- the elements after.
-type SplitPPExprList = Maybe ([PPExpr], AppPPExpr, [PPExpr])
+type SplitPPExprList ann = Maybe ([PPExpr ann], AppPPExpr ann, [PPExpr ann])
 
-findExprToRemove :: [PPExpr] -> SplitPPExprList
+findExprToRemove :: [PPExpr ann] -> SplitPPExprList ann
 findExprToRemove exprs0 = go [] exprs0 Nothing
-  where go :: [PPExpr] -> [PPExpr] -> SplitPPExprList -> SplitPPExprList
+  where go :: [PPExpr ann] -> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
         go _ [] mr = mr
         go prev (e@FixedPPExpr{} : exprs) mr = do
           go (e:prev) exprs mr
@@ -951,7 +951,7 @@ findExprToRemove exprs0 = go [] exprs0 Nothing
           go (AppPPExpr a:prev) exprs (Just (reverse prev, a, exprs))
 
 
-ppExpr' :: forall t tp s . Expr t tp -> PPExprOpts -> ST s ([Doc], PPExpr)
+ppExpr' :: forall t tp s ann. Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann)
 ppExpr' e0 o = do
   let max_width = ppExpr_maxWidth o
   let use_decimal = ppExpr_useDecimal o
@@ -966,11 +966,11 @@ ppExpr' e0 o = do
 
   bindingsRef <- newSTRef Seq.empty
 
-  visited <- H.new :: ST s (H.HashTable s PPIndex PPExpr)
+  visited <- H.new :: ST s (H.HashTable s PPIndex (PPExpr ann))
   visited_fns <- H.new :: ST s (H.HashTable s Word64 Text)
 
   let -- Add a binding to the list of bindings
-      addBinding :: AppPPExpr -> ST s PPExpr
+      addBinding :: AppPPExpr ann -> ST s (PPExpr ann)
       addBinding a = do
         let idx = apeIndex a
         cnt <- Seq.length <$> readSTRef bindingsRef
@@ -983,8 +983,9 @@ ppExpr' e0 o = do
                    ExprPPIndex e -> "v" ++ show e
                    RatPPIndex _ -> "r" ++ show cnt
         let lhs = parenIf False (text nm) (text <$> args)
-        let doc = text "--" <+> pretty (plSourceLoc (apeLoc a)) <$$>
-                  lhs <+> text "=" <+> uncurry (parenIf False) (apeDoc a)
+        let doc = vcat
+                  [ text "--" <+> pretty (plSourceLoc (apeLoc a))
+                  , lhs <+> text "=" <+> uncurry (parenIf False) (apeDoc a) ]
         modifySTRef' bindingsRef (Seq.|> doc)
         let len = length nm + sum ((\arg_s -> length arg_s + 1) <$> args)
         let nm_expr = FixedPPExpr (text nm) (map text args) len
@@ -992,8 +993,8 @@ ppExpr' e0 o = do
         return nm_expr
 
   let fixLength :: Int
-                -> [PPExpr]
-                -> ST s ([PPExpr], Int)
+                -> [PPExpr ann]
+                -> ST s ([PPExpr ann], Int)
       fixLength cur_width exprs
         | cur_width > max_width
         , Just (prev_e, a, next_e) <- findExprToRemove exprs = do
@@ -1004,7 +1005,7 @@ ppExpr' e0 o = do
         return $! (exprs, cur_width)
 
   -- Pretty print an argument.
-  let renderArg :: PrettyArg (Expr t) -> ST s PPExpr
+  let renderArg :: PrettyArg (Expr t) -> ST s (PPExpr ann)
       renderArg (PrettyArg e) = getBindings e
       renderArg (PrettyText txt) = return (textPPExpr txt)
       renderArg (PrettyFunc nm args) =
@@ -1018,7 +1019,7 @@ ppExpr' e0 o = do
                 -> ProgramLoc
                 -> Text
                 -> [PrettyArg (Expr t)]
-                -> ST s AppPPExpr
+                -> ST s (AppPPExpr ann)
       renderApp idx loc nm args = Ex.assert (not (Prelude.null args)) $ do
         exprs0 <- traverse renderArg args
         -- Get width not including parenthesis of outer app.
@@ -1034,7 +1035,7 @@ ppExpr' e0 o = do
       cacheResult :: PPIndex
                   -> ProgramLoc
                   -> PrettyApp (Expr t)
-                  -> ST s PPExpr
+                  -> ST s (PPExpr ann)
       cacheResult _ _ (nm,[]) = do
         return (textPPExpr nm)
       cacheResult idx loc (nm,args) = do
@@ -1073,7 +1074,7 @@ ppExpr' e0 o = do
 
       -- Collect definitions for all applications that occur multiple times
       -- in term.
-      getBindings :: Expr t u -> ST s PPExpr
+      getBindings :: Expr t u -> ST s (PPExpr ann)
       getBindings (SemiRingLiteral sr x l) =
         case sr of
           SR.SemiRingNatRepr ->
@@ -4696,3 +4697,6 @@ mkFreshUninterpFnApp sym str_fn_name args ret_type = do
   let arg_types = fmapFC exprType args
   fn <- freshTotalUninterpFn sym fn_name arg_types ret_type
   applySymFn sym fn args
+
+text :: String -> Doc ann
+text = pretty
diff --git a/what4/src/What4/Expr/MATLAB.hs b/what4/src/What4/Expr/MATLAB.hs
index 4d2510ab..51186bda 100644
--- a/what4/src/What4/Expr/MATLAB.hs
+++ b/what4/src/What4/Expr/MATLAB.hs
@@ -45,7 +45,7 @@ import           Data.Parameterized.Classes
 import           Data.Parameterized.Context as Ctx
 import           Data.Parameterized.TH.GADT
 import           Data.Parameterized.TraversableFC
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import           Prettyprinter
 
 import           What4.BaseTypes
 import           What4.Interface
@@ -664,71 +664,74 @@ matlabSolverReturnType f =
     CplxCosFn            -> knownRepr
     CplxTanFn            -> knownRepr
 
-ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc
+ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc ann
 ppMatlabSolverFn f =
   case f of
-    BoolOrFn             -> text "bool_or"
-    IsIntegerFn          -> text "is_integer"
-    NatLeFn              -> text "nat_le"
-    IntLeFn              -> text "int_le"
-    BVToNatFn w          -> parens $ text "bv_to_nat" <+> text (show w)
-    SBVToIntegerFn w     -> parens $ text "sbv_to_int" <+> text (show w)
-    NatToIntegerFn       -> text "nat_to_integer"
-    IntegerToNatFn       -> text "integer_to_nat"
-    IntegerToRealFn      -> text "integer_to_real"
-    RealToIntegerFn      -> text "real_to_integer"
-    PredToIntegerFn      -> text "pred_to_integer"
-    NatSeqFn  b i        -> parens $ text "nat_seq"  <+> printSymExpr b <+> printSymExpr i
-    RealSeqFn b i        -> parens $ text "real_seq" <+> printSymExpr b <+> printSymExpr i
+    BoolOrFn             -> pretty "bool_or"
+    IsIntegerFn          -> pretty "is_integer"
+    NatLeFn              -> pretty "nat_le"
+    IntLeFn              -> pretty "int_le"
+    BVToNatFn w          -> parens $ pretty "bv_to_nat" <+> ppNatRepr w
+    SBVToIntegerFn w     -> parens $ pretty "sbv_to_int" <+> ppNatRepr w
+    NatToIntegerFn       -> pretty "nat_to_integer"
+    IntegerToNatFn       -> pretty "integer_to_nat"
+    IntegerToRealFn      -> pretty "integer_to_real"
+    RealToIntegerFn      -> pretty "real_to_integer"
+    PredToIntegerFn      -> pretty "pred_to_integer"
+    NatSeqFn  b i        -> parens $ pretty "nat_seq"  <+> printSymExpr b <+> printSymExpr i
+    RealSeqFn b i        -> parens $ pretty "real_seq" <+> printSymExpr b <+> printSymExpr i
     IndicesInRange _ bnds ->
-      parens (text "indices_in_range" <+> sep (toListFC printSymExpr bnds))
-    IsEqFn{}             -> text "is_eq"
+      parens (pretty "indices_in_range" <+> sep (toListFC printSymExpr bnds))
+    IsEqFn{}             -> pretty "is_eq"
 
-    BVIsNonZeroFn w      -> parens $ text "bv_is_nonzero" <+> text (show w)
-    ClampedIntNegFn w    -> parens $ text "clamped_int_neg" <+> text (show w)
-    ClampedIntAbsFn w    -> parens $ text "clamped_neg_abs" <+> text (show w)
-    ClampedIntAddFn w    -> parens $ text "clamped_int_add" <+> text (show w)
-    ClampedIntSubFn w    -> parens $ text "clamped_int_sub" <+> text (show w)
-    ClampedIntMulFn w    -> parens $ text "clamped_int_mul" <+> text (show w)
-    ClampedUIntAddFn w   -> parens $ text "clamped_uint_add" <+> text (show w)
-    ClampedUIntSubFn w   -> parens $ text "clamped_uint_sub" <+> text (show w)
-    ClampedUIntMulFn w   -> parens $ text "clamped_uint_mul" <+> text (show w)
+    BVIsNonZeroFn w      -> parens $ pretty "bv_is_nonzero" <+> ppNatRepr w
+    ClampedIntNegFn w    -> parens $ pretty "clamped_int_neg" <+> ppNatRepr w
+    ClampedIntAbsFn w    -> parens $ pretty "clamped_neg_abs" <+> ppNatRepr w
+    ClampedIntAddFn w    -> parens $ pretty "clamped_int_add" <+> ppNatRepr w
+    ClampedIntSubFn w    -> parens $ pretty "clamped_int_sub" <+> ppNatRepr w
+    ClampedIntMulFn w    -> parens $ pretty "clamped_int_mul" <+> ppNatRepr w
+    ClampedUIntAddFn w   -> parens $ pretty "clamped_uint_add" <+> ppNatRepr w
+    ClampedUIntSubFn w   -> parens $ pretty "clamped_uint_sub" <+> ppNatRepr w
+    ClampedUIntMulFn w   -> parens $ pretty "clamped_uint_mul" <+> ppNatRepr w
 
-    IntSetWidthFn i o    -> parens $ text "int_set_width"  <+> text (show i) <+> text (show o)
-    UIntSetWidthFn i o   -> parens $ text "uint_set_width" <+> text (show i) <+> text (show o)
-    UIntToIntFn i o      -> parens $ text "uint_to_int"  <+> text (show i) <+> text (show o)
-    IntToUIntFn i o      -> parens $ text "int_to_uint"  <+> text (show i) <+> text (show o)
+    IntSetWidthFn i o    -> parens $ pretty "int_set_width"  <+> pretty (show i) <+> pretty (show o)
+    UIntSetWidthFn i o   -> parens $ pretty "uint_set_width" <+> pretty (show i) <+> pretty (show o)
+    UIntToIntFn i o      -> parens $ pretty "uint_to_int"  <+> pretty (show i) <+> pretty (show o)
+    IntToUIntFn i o      -> parens $ pretty "int_to_uint"  <+> pretty (show i) <+> pretty (show o)
 
-    RealCosFn            -> text "real_cos"
-    RealSinFn            -> text "real_sin"
-    RealIsNonZeroFn      -> text "real_is_nonzero"
+    RealCosFn            -> pretty "real_cos"
+    RealSinFn            -> pretty "real_sin"
+    RealIsNonZeroFn      -> pretty "real_is_nonzero"
 
-    RealToSBVFn w        -> parens $ text "real_to_sbv" <+> text (show w)
-    RealToUBVFn w        -> parens $ text "real_to_sbv" <+> text (show w)
-    PredToBVFn  w        -> parens $ text "pred_to_bv"  <+> text (show w)
+    RealToSBVFn w        -> parens $ pretty "real_to_sbv" <+> ppNatRepr w
+    RealToUBVFn w        -> parens $ pretty "real_to_sbv" <+> ppNatRepr w
+    PredToBVFn  w        -> parens $ pretty "pred_to_bv"  <+> ppNatRepr w
 
-    CplxIsNonZeroFn      -> text "cplx_is_nonzero"
-    CplxIsRealFn         -> text "cplx_is_real"
-    RealToComplexFn      -> text "real_to_complex"
-    RealPartOfCplxFn     -> text "real_part_of_complex"
-    ImagPartOfCplxFn     -> text "imag_part_of_complex"
+    CplxIsNonZeroFn      -> pretty "cplx_is_nonzero"
+    CplxIsRealFn         -> pretty "cplx_is_real"
+    RealToComplexFn      -> pretty "real_to_complex"
+    RealPartOfCplxFn     -> pretty "real_part_of_complex"
+    ImagPartOfCplxFn     -> pretty "imag_part_of_complex"
 
-    CplxNegFn            -> text "cplx_neg"
-    CplxAddFn            -> text "cplx_add"
-    CplxSubFn            -> text "cplx_sub"
-    CplxMulFn            -> text "cplx_mul"
+    CplxNegFn            -> pretty "cplx_neg"
+    CplxAddFn            -> pretty "cplx_add"
+    CplxSubFn            -> pretty "cplx_sub"
+    CplxMulFn            -> pretty "cplx_mul"
 
-    CplxRoundFn          -> text "cplx_round"
-    CplxFloorFn          -> text "cplx_floor"
-    CplxCeilFn           -> text "cplx_ceil"
-    CplxMagFn            -> text "cplx_mag"
-    CplxSqrtFn           -> text "cplx_sqrt"
-    CplxExpFn            -> text "cplx_exp"
-    CplxLogFn            -> text "cplx_log"
-    CplxLogBaseFn b      -> parens $ text "cplx_log_base" <+> text (show b)
-    CplxSinFn            -> text "cplx_sin"
-    CplxCosFn            -> text "cplx_cos"
-    CplxTanFn            -> text "cplx_tan"
+    CplxRoundFn          -> pretty "cplx_round"
+    CplxFloorFn          -> pretty "cplx_floor"
+    CplxCeilFn           -> pretty "cplx_ceil"
+    CplxMagFn            -> pretty "cplx_mag"
+    CplxSqrtFn           -> pretty "cplx_sqrt"
+    CplxExpFn            -> pretty "cplx_exp"
+    CplxLogFn            -> pretty "cplx_log"
+    CplxLogBaseFn b      -> parens $ pretty "cplx_log_base" <+> pretty (show b)
+    CplxSinFn            -> pretty "cplx_sin"
+    CplxCosFn            -> pretty "cplx_cos"
+    CplxTanFn            -> pretty "cplx_tan"
+
+ppNatRepr :: NatRepr w -> Doc ann
+ppNatRepr w = pretty (show w)
 
 -- | Test 'MatlabSolverFn' values for equality.
 testSolverFnEq :: TestEquality f
diff --git a/what4/src/What4/Expr/VarIdentification.hs b/what4/src/What4/Expr/VarIdentification.hs
index afb4d935..97422414 100644
--- a/what4/src/What4/Expr/VarIdentification.hs
+++ b/what4/src/What4/Expr/VarIdentification.hs
@@ -57,7 +57,7 @@ import qualified Data.Sequence as Seq
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Word
-import           Text.PrettyPrint.ANSI.Leijen
+import           Prettyprinter (Doc)
 
 import           What4.BaseTypes
 import           What4.Expr.AppTheory
@@ -96,7 +96,7 @@ data CollectedVarInfo t
                       , _forallQuantifiers :: !(QuantifierInfoMap t)
                       , _latches  :: !(Set (Some (ExprBoundVar t)))
                         -- | List of errors found during parsing.
-                      , _varErrors :: !(Seq Doc)
+                      , _varErrors :: !(Seq (Doc ()))
                       }
 
 -- | Describes types of functionality required by solver based on the problem.
@@ -121,7 +121,7 @@ forallQuantifiers = lens _forallQuantifiers (\s v -> s { _forallQuantifiers = v
 latches :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
 latches = lens _latches (\s v -> s { _latches = v })
 
-varErrors :: Simple Lens (CollectedVarInfo t) (Seq Doc)
+varErrors :: Simple Lens (CollectedVarInfo t) (Seq (Doc ()))
 varErrors = lens _varErrors (\s v -> s { _varErrors = v })
 
 -- | Return variables needed to define element as a predicate
diff --git a/what4/src/What4/FunctionName.hs b/what4/src/What4/FunctionName.hs
index 53348b5a..1cf290fe 100644
--- a/what4/src/What4/FunctionName.hs
+++ b/what4/src/What4/FunctionName.hs
@@ -21,7 +21,7 @@ module What4.FunctionName
 import           Data.Hashable
 import           Data.String
 import qualified Data.Text as Text
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 ------------------------------------------------------------------------
 -- FunctionName
@@ -38,7 +38,7 @@ instance Show FunctionName where
   show (FunctionName nm) = Text.unpack nm
 
 instance PP.Pretty FunctionName where
-  pretty (FunctionName nm) = PP.text (Text.unpack nm)
+  pretty (FunctionName nm) = PP.pretty nm
 
 -- | Name of function for starting simulator.
 startFunctionName :: FunctionName
diff --git a/what4/src/What4/Interface.hs b/what4/src/What4/Interface.hs
index 4b83f05f..427da197 100644
--- a/what4/src/What4/Interface.hs
+++ b/what4/src/What4/Interface.hs
@@ -183,7 +183,7 @@ import           Data.Ratio
 import           Data.Scientific (Scientific)
 import           GHC.Generics (Generic)
 import           Numeric.Natural
-import           Text.PrettyPrint.ANSI.Leijen (Doc)
+import           Prettyprinter (Doc)
 
 import           What4.BaseTypes
 import           What4.Config
@@ -348,7 +348,7 @@ class HasAbsValue e => IsExpr e where
       BaseBVRepr w -> w
 
   -- | Print a sym expression for debugging or display purposes.
-  printSymExpr :: e tp -> Doc
+  printSymExpr :: e tp -> Doc ann
 
 
 newtype ArrayResultWrapper f idx tp =
diff --git a/what4/src/What4/InterpretedFloatingPoint.hs b/what4/src/What4/InterpretedFloatingPoint.hs
index fcf5d264..47b146c1 100644
--- a/what4/src/What4/InterpretedFloatingPoint.hs
+++ b/what4/src/What4/InterpretedFloatingPoint.hs
@@ -50,7 +50,7 @@ import Data.Parameterized.TH.GADT
 import Data.Ratio
 import Data.Word ( Word16, Word64 )
 import GHC.TypeNats
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
 
 import What4.BaseTypes
 import What4.Interface
@@ -97,7 +97,7 @@ instance Hashable (FloatInfoRepr fi) where
   hashWithSalt = $(structuralHashWithSalt [t|FloatInfoRepr|] [])
 
 instance Pretty (FloatInfoRepr fi) where
-  pretty = text . show
+  pretty = pretty . show
 instance Show (FloatInfoRepr fi) where
   showsPrec = $(structuralShowsPrec [t|FloatInfoRepr|])
 instance ShowF FloatInfoRepr
diff --git a/what4/src/What4/ProgramLoc.hs b/what4/src/What4/ProgramLoc.hs
index 2b4fea3a..771a8c8b 100644
--- a/what4/src/What4/ProgramLoc.hs
+++ b/what4/src/What4/ProgramLoc.hs
@@ -38,7 +38,7 @@ import           Data.Text (Text)
 import qualified Data.Text as Text
 import           Data.Word
 import           Numeric (showHex)
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 import           What4.FunctionName
 
@@ -73,23 +73,23 @@ startOfFile path = sourcePos path 1 0
 
 instance PP.Pretty Position where
   pretty (SourcePos path l c) =
-    PP.text (Text.unpack path)
-      PP.<> PP.colon PP.<> PP.int l
-      PP.<> PP.colon PP.<> PP.int c
+    PP.pretty path
+      PP.<> PP.colon PP.<> PP.pretty l
+      PP.<> PP.colon PP.<> PP.pretty c
   pretty (BinaryPos path addr) =
-    PP.text (Text.unpack path) PP.<> PP.colon PP.<>
-      PP.text "0x" PP.<> PP.text (showHex addr "")
-  pretty (OtherPos txt) = PP.text (Text.unpack txt)
-  pretty InternalPos = PP.text "internal"
+    PP.pretty path PP.<> PP.colon PP.<>
+      PP.pretty "0x" PP.<> PP.pretty (showHex addr "")
+  pretty (OtherPos txt) = PP.pretty txt
+  pretty InternalPos = PP.pretty "internal"
 
-ppNoFileName :: Position -> PP.Doc
+ppNoFileName :: Position -> PP.Doc ann
 ppNoFileName (SourcePos _ l c) =
-  PP.int l PP.<> PP.colon PP.<> PP.int c
+  PP.pretty l PP.<> PP.colon PP.<> PP.pretty c
 ppNoFileName (BinaryPos _ addr) =
-  PP.text (showHex addr "")
+  PP.pretty (showHex addr "")
 ppNoFileName (OtherPos msg) =
-  PP.text (Text.unpack msg)
-ppNoFileName InternalPos = PP.text "internal"
+  PP.pretty msg
+ppNoFileName InternalPos = PP.pretty "internal"
 
 ------------------------------------------------------------------------
 -- Posd
diff --git a/what4/src/What4/Protocol/Online.hs b/what4/src/What4/Protocol/Online.hs
index a3cd89f8..75e3223c 100644
--- a/what4/src/What4/Protocol/Online.hs
+++ b/what4/src/What4/Protocol/Online.hs
@@ -48,12 +48,12 @@ import           Data.Proxy
 import           Data.IORef
 import           Data.Text (Text)
 import qualified Data.Text.Lazy as LazyText
+import           Prettyprinter
 import           System.Exit
 import           System.IO
 import qualified System.IO.Streams as Streams
 import           System.Process
                    (ProcessHandle, terminateProcess, waitForProcess)
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
 
 import           What4.Expr
 import           What4.Interface (SolverEvent(..))
@@ -361,7 +361,7 @@ getUnsatAssumptions :: SMTReadWriter solver => SolverProcess scope solver -> IO
 getUnsatAssumptions proc =
   do let conn = solverConn proc
      unless (supportedFeatures conn `hasProblemFeature` useUnsatAssumptions) $
-       fail $ show $ text (smtWriterName conn) <+> text "is not configured to produce UNSAT assumption lists"
+       fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce UNSAT assumption lists"
      addCommandNoAck conn (getUnsatAssumptionsCommand conn)
      smtUnsatAssumptionsResult conn (solverResponse proc)
 
@@ -372,7 +372,7 @@ getUnsatCore :: SMTReadWriter solver => SolverProcess scope solver -> IO [Text]
 getUnsatCore proc =
   do let conn = solverConn proc
      unless (supportedFeatures conn `hasProblemFeature` useUnsatCores) $
-       fail $ show $ text (smtWriterName conn) <+> text "is not configured to produce UNSAT cores"
+       fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce UNSAT cores"
      addCommandNoAck conn (getUnsatCoreCommand conn)
      smtUnsatCoreResult conn (solverResponse proc)
 
diff --git a/what4/src/What4/Protocol/PolyRoot.hs b/what4/src/What4/Protocol/PolyRoot.hs
index 692fe58a..aefd889d 100644
--- a/what4/src/What4/Protocol/PolyRoot.hs
+++ b/what4/src/What4/Protocol/PolyRoot.hs
@@ -32,7 +32,7 @@ import           Data.Text (Text)
 import qualified Data.Text as Text
 
 import qualified Data.Vector as V
-import           Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>))
+import           Prettyprinter as PP
 
 atto_angle :: Atto.Parser a -> Atto.Parser a
 atto_angle p = Atto.char '<' *> p <* Atto.char '>'
@@ -47,19 +47,19 @@ newtype SingPoly coef = SingPoly (V.Vector coef)
 instance (Ord coef, Num coef, Pretty coef) => Pretty (SingPoly coef) where
   pretty (SingPoly v) =
     case V.findIndex (/= 0) v of
-      Nothing -> text "0"
+      Nothing -> pretty "0"
       Just j -> go (V.length v - 1)
         where ppc c | c < 0 = parens (pretty c)
                     | otherwise = pretty c
 
-              ppi 1 = text "*x"
-              ppi i = text "*x^" <> pretty i
+              ppi 1 = pretty "*x"
+              ppi i = pretty "*x^" <> pretty i
 
               go 0 = ppc (v V.! 0)
               go i | seq i False = error "pretty SingPoly"
                    | i == j = ppc (v V.! i) <> ppi i
                    | v V.! i == 0 = go (i-1)
-                   | otherwise = ppc (v V.! i) <> ppi i <+> text "+" <+> go (i-1)
+                   | otherwise = ppc (v V.! i) <> ppi i <+> pretty "+" <+> go (i-1)
 
 fromList :: [c] -> SingPoly c
 fromList = SingPoly . V.fromList
diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs
index 825d3d99..124dacc4 100644
--- a/what4/src/What4/Protocol/SMTLib2.hs
+++ b/what4/src/What4/Protocol/SMTLib2.hs
@@ -121,7 +121,7 @@ import qualified System.IO.Streams as Streams
 import qualified System.IO.Streams.Attoparsec.Text as Streams
 import           Data.Versions (Version(..))
 import qualified Data.Versions as Versions
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 import           Prelude hiding (writeFile)
 
@@ -1167,14 +1167,17 @@ solverMaxVersions = []
 data SolverVersionCheckError =
   UnparseableVersion Versions.ParsingError
 
-ppSolverVersionCheckError :: SolverVersionCheckError -> PP.Doc
-ppSolverVersionCheckError =
-  (PP.text "Unexpected error while checking solver version: " PP.<$$>) .
-  \case
-    UnparseableVersion parseErr -> PP.cat $ map PP.text
-      [ "Couldn't parse solver version number: "
-      , show parseErr
-      ]
+ppSolverVersionCheckError :: SolverVersionCheckError -> PP.Doc ann
+ppSolverVersionCheckError err =
+  PP.vsep
+  [ "Unexpected error while checking solver version:"
+  , case err of
+      UnparseableVersion parseErr ->
+        PP.hsep $ map PP.pretty
+        [ "Couldn't parse solver version number:"
+        , show parseErr
+        ]
+  ]
 
 data SolverVersionError =
   SolverVersionError
@@ -1184,9 +1187,10 @@ data SolverVersionError =
   }
   deriving (Eq, Ord)
 
-ppSolverVersionError :: SolverVersionError -> PP.Doc
-ppSolverVersionError err = PP.vcat $ map PP.text
-  [ "Solver did not meet version bound restrictions: "
+ppSolverVersionError :: SolverVersionError -> PP.Doc ann
+ppSolverVersionError err =
+  PP.vsep $ map PP.pretty
+  [ "Solver did not meet version bound restrictions:"
   , "Lower bound (inclusive): " ++ na (show <$> vMin err)
   , "Upper bound (non-inclusive): " ++ na (show <$> vMax err)
   , "Actual version: " ++ show (vActual err)
diff --git a/what4/src/What4/Protocol/SMTWriter.hs b/what4/src/What4/Protocol/SMTWriter.hs
index 5bbb5766..0ee24d4e 100644
--- a/what4/src/What4/Protocol/SMTWriter.hs
+++ b/what4/src/What4/Protocol/SMTWriter.hs
@@ -132,7 +132,7 @@ import qualified Data.Text.Lazy as Lazy
 import           Data.Word
 
 import           Numeric.Natural
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
+import           Prettyprinter hiding (Unbounded)
 import           System.IO.Streams (OutputStream, InputStream)
 import qualified System.IO.Streams as Streams
 
@@ -1484,9 +1484,11 @@ sbvIntTerm w0 x0 = sumExpr (signed_offset : go w0 x0 (natValue w0 - 2))
 unsupportedTerm  :: MonadFail m => Expr t tp -> m a
 unsupportedTerm e =
   fail $ show $
-    text "Cannot generate solver output for term generated at"
-      <+> pretty (plSourceLoc (exprLoc e)) <> text ":" <$$>
-    indent 2 (pretty e)
+  vcat
+  [ text "Cannot generate solver output for term generated at"
+      <+> pretty (plSourceLoc (exprLoc e)) <> text ":"
+  , indent 2 (pretty e)
+  ]
 
 -- | Checks whether a variable is supported.
 --
@@ -1575,22 +1577,24 @@ checkArgumentTypes conn types = do
 -- | This generates an error message from a solver and a type error.
 --
 -- It issed for error reporting
-type SMTSource = String -> BaseTypeError -> Doc
+type SMTSource ann = String -> BaseTypeError -> Doc ann
 
-ppBaseTypeError :: BaseTypeError -> Doc
+ppBaseTypeError :: BaseTypeError -> Doc ann
 ppBaseTypeError ComplexTypeUnsupported = text "complex values"
 ppBaseTypeError ArrayUnsupported = text "arrays encoded as a functions"
 ppBaseTypeError (StringTypeUnsupported (Some si)) = text ("string values " ++ show si)
 
-eltSource :: Expr t tp -> SMTSource
+eltSource :: Expr t tp -> SMTSource ann
 eltSource e solver_name cause =
-  text solver_name <+>
-  text "does not support" <+> ppBaseTypeError cause <>
-  text ", and cannot interpret the term generated at" <+>
-  pretty (plSourceLoc (exprLoc e)) <> text ":" <$$>
-  indent 2 (pretty e) <> text "."
+  vcat
+  [ text solver_name <+>
+    text "does not support" <+> ppBaseTypeError cause <>
+    text ", and cannot interpret the term generated at" <+>
+    pretty (plSourceLoc (exprLoc e)) <> text ":"
+  , indent 2 (pretty e) <> text "."
+  ]
 
-fnSource :: SolverSymbol -> ProgramLoc -> SMTSource
+fnSource :: SolverSymbol -> ProgramLoc -> SMTSource ann
 fnSource fn_name loc solver_name cause =
   text solver_name <+>
   text "does not support" <+> ppBaseTypeError cause <>
@@ -1603,7 +1607,7 @@ fnSource fn_name loc solver_name cause =
 -- returned by functions.
 evalFirstClassTypeRepr :: MonadFail m
                        => WriterConn t h
-                       -> SMTSource
+                       -> SMTSource ann
                        -> BaseTypeRepr tp
                        -> m (TypeMap tp)
 evalFirstClassTypeRepr conn src base_tp =
@@ -1895,10 +1899,13 @@ appSMTExpr ae = do
          let ytp = smtExprType ye
 
          let checkArrayType z (FnArrayTypeMap{}) = do
-               fail $ show $ text (smtWriterName conn) <+>
-                 text "does not support checking equality for the array generated at"
-                 <+> pretty (plSourceLoc (exprLoc z)) <> text ":" <$$>
-                 indent 2 (pretty z)
+               fail $ show $
+                 vcat
+                 [ text (smtWriterName conn) <+>
+                   text "does not support checking equality for the array generated at"
+                   <+> pretty (plSourceLoc (exprLoc z)) <> text ":"
+                 , indent 2 (pretty z)
+                 ]
              checkArrayType _ _ = return ()
 
          checkArrayType x xtp
@@ -3059,3 +3066,6 @@ smtExprGroundEvalFn conn smtFns = do
 
 
   return $ GroundEvalFn cachedEval
+
+text :: String -> Doc ann
+text = pretty
diff --git a/what4/src/What4/Solver/Adapter.hs b/what4/src/What4/Solver/Adapter.hs
index 774602b1..153752d7 100644
--- a/what4/src/What4/Solver/Adapter.hs
+++ b/what4/src/What4/Solver/Adapter.hs
@@ -29,7 +29,7 @@ import           Data.IORef
 import qualified Data.Map as Map
 import qualified Data.Text as T
 import           System.IO
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 
 import           What4.BaseTypes
@@ -129,7 +129,7 @@ solverAdapterOptions xs@(def:_) =
  vals ref = Map.fromList (map (f ref) xs)
  sty ref = mkOpt defaultSolverAdapter
                  (listOptSty (vals ref))
-                 (Just (PP.text "Indicates which solver to use for check-sat queries"))
+                 (Just (PP.pretty "Indicates which solver to use for check-sat queries"))
                  (Just (ConcreteString (UnicodeLiteral (T.pack (solver_adapter_name def)))))
 
 -- | Test the ability to interact with a solver by peforming a check-sat query
diff --git a/what4/src/What4/Solver/Boolector.hs b/what4/src/What4/Solver/Boolector.hs
index cb42cf8a..633ade95 100644
--- a/what4/src/What4/Solver/Boolector.hs
+++ b/what4/src/What4/Solver/Boolector.hs
@@ -28,7 +28,6 @@ module What4.Solver.Boolector
 
 import           Control.Monad
 import           Data.Bits ( (.|.) )
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
 
 import           What4.BaseTypes
 import           What4.Config
@@ -57,7 +56,7 @@ boolectorOptions =
   [ mkOpt
       boolectorPath
       executablePathOptSty
-      (Just (PP.text "Path to boolector executable"))
+      (Just "Path to boolector executable")
       (Just (ConcreteString "boolector"))
   ]
 
diff --git a/what4/src/What4/Solver/CVC4.hs b/what4/src/What4/Solver/CVC4.hs
index 56004584..442e6628 100644
--- a/what4/src/What4/Solver/CVC4.hs
+++ b/what4/src/What4/Solver/CVC4.hs
@@ -33,7 +33,6 @@ import           Data.Bits
 import           Data.String
 import           System.IO
 import qualified System.IO.Streams as Streams
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
 
 import           What4.BaseTypes
 import           What4.Config
@@ -72,12 +71,12 @@ cvc4Options :: [ConfigDesc]
 cvc4Options =
   [ mkOpt cvc4Path
           executablePathOptSty
-          (Just (PP.text "Path to CVC4 executable"))
+          (Just "Path to CVC4 executable")
           (Just (ConcreteString "cvc4"))
   , intWithRangeOpt cvc4RandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1)
   , mkOpt cvc4Timeout
           integerOptSty
-          (Just (PP.text "Per-check timeout in milliseconds (zero is none)"))
+          (Just "Per-check timeout in milliseconds (zero is none)")
           (Just (ConcreteInteger 0))
   ]
 
diff --git a/what4/src/What4/Solver/DReal.hs b/what4/src/What4/Solver/DReal.hs
index c54b9556..6ded04e8 100644
--- a/what4/src/What4/Solver/DReal.hs
+++ b/what4/src/What4/Solver/DReal.hs
@@ -45,7 +45,6 @@ import           System.IO.Error
 import qualified System.IO.Streams as Streams
 import qualified System.IO.Streams.Attoparsec as Streams
 import           System.Process
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
 
 import           What4.BaseTypes
 import           What4.Config
@@ -73,7 +72,7 @@ drealOptions =
   [ mkOpt
       drealPath
       executablePathOptSty
-      (Just (PP.text "Path to dReal executable"))
+      (Just "Path to dReal executable")
       (Just (ConcreteString "dreal"))
   ]
 
diff --git a/what4/src/What4/Solver/STP.hs b/what4/src/What4/Solver/STP.hs
index 3787c722..c8c2d1bd 100644
--- a/what4/src/What4/Solver/STP.hs
+++ b/what4/src/What4/Solver/STP.hs
@@ -23,7 +23,6 @@ module What4.Solver.STP
   ) where
 
 import           Data.Bits
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
 
 import           What4.BaseTypes
 import           What4.Config
@@ -55,7 +54,7 @@ stpOptions :: [ConfigDesc]
 stpOptions =
   [ mkOpt stpPath
           executablePathOptSty
-          (Just (PP.text "Path to STP executable."))
+          (Just "Path to STP executable.")
           (Just (ConcreteString "stp"))
   , intWithRangeOpt stpRandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1)
   ]
diff --git a/what4/src/What4/Solver/Yices.hs b/what4/src/What4/Solver/Yices.hs
index 3fea541e..3fddaed3 100644
--- a/what4/src/What4/Solver/Yices.hs
+++ b/what4/src/What4/Solver/Yices.hs
@@ -99,7 +99,7 @@ import           System.Exit
 import           System.IO
 import qualified System.IO.Streams as Streams
 import qualified System.IO.Streams.Attoparsec.Text as Streams
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 import           What4.BaseTypes
 import           What4.Config
@@ -935,22 +935,22 @@ yicesOptions =
   [ mkOpt
       yicesPath
       executablePathOptSty
-      (Just (PP.text "Yices executable path"))
+      (Just "Yices executable path")
       (Just (ConcreteString "yices"))
   , mkOpt
       yicesEnableMCSat
       boolOptSty
-      (Just (PP.text "Enable the Yices MCSAT solving engine"))
+      (Just "Enable the Yices MCSAT solving engine")
       (Just (ConcreteBool False))
   , mkOpt
       yicesEnableInteractive
       boolOptSty
-      (Just (PP.text "Enable Yices interactive mode (needed to support timeouts)"))
+      (Just "Enable Yices interactive mode (needed to support timeouts)")
       (Just (ConcreteBool False))
   , mkOpt
       yicesGoalTimeout
       integerOptSty
-      (Just (PP.text "Set a per-goal timeout"))
+      (Just "Set a per-goal timeout")
       (Just (ConcreteInteger 0))
   ]
   ++ yicesInternalOptions
@@ -1073,8 +1073,8 @@ checkSupportedByYices p = do
   -- Check no errors where reported in result.
   let errors = toList (varInfo^.varErrors)
   when (not (null errors)) $ do
-    fail $ show $ PP.text "This formula is not supported by yices:" PP.<$$>
-           PP.indent 2 (PP.vcat errors)
+    fail $ show $
+      PP.vcat ["This formula is not supported by yices:", PP.indent 2 (PP.vcat errors)]
 
   return $! varInfo^.problemFeatures
 
diff --git a/what4/src/What4/Solver/Z3.hs b/what4/src/What4/Solver/Z3.hs
index a26c16dd..21d842fe 100644
--- a/what4/src/What4/Solver/Z3.hs
+++ b/what4/src/What4/Solver/Z3.hs
@@ -31,7 +31,6 @@ import           Control.Monad ( when )
 import           Data.Bits
 import           Data.String
 import           System.IO
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
 
 import           What4.BaseTypes
 import           What4.Concrete
@@ -63,12 +62,12 @@ z3Options =
   [ mkOpt
       z3Path
       executablePathOptSty
-      (Just (PP.text "Z3 executable path"))
+      (Just "Z3 executable path")
       (Just (ConcreteString "z3"))
   , mkOpt
       z3Timeout
       integerOptSty
-      (Just (PP.text "Per-check timeout in milliseconds (zero is none)"))
+      (Just "Per-check timeout in milliseconds (zero is none)")
       (Just (ConcreteInteger 0))
   ]
 
diff --git a/what4/what4.cabal b/what4/what4.cabal
index b7ffa255..6e304a15 100644
--- a/what4/what4.cabal
+++ b/what4/what4.cabal
@@ -52,7 +52,6 @@ library
   build-depends:
     base >= 4.8 && < 5,
     attoparsec >= 0.13,
-    ansi-wl-pprint >= 0.6.8,
     bimap >= 0.2,
     bifunctors >= 5,
     bv-sized >= 1.0.0,
@@ -73,6 +72,7 @@ library
     mtl >= 2.2.1,
     panic >= 0.3,
     parameterized-utils >= 2.1 && < 2.2,
+    prettyprinter >= 1.7.0,
     process >= 1.2,
     scientific >= 0.3.6,
     temporary >= 1.2,