diff --git a/Codec/TPTP/Base.hs b/Codec/TPTP/Base.hs
--- a/Codec/TPTP/Base.hs
+++ b/Codec/TPTP/Base.hs
@@ -2,24 +2,16 @@
   , StandaloneDeriving
   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
-  , OverlappingInstances, ScopedTypeVariables
+  , ScopedTypeVariables
   #-}
 
 module Codec.TPTP.Base where
 
-#ifndef MIN_VERSION_transformers
-#define MIN_VERSION_transformers(a,b,c) 1
-#endif
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(a,b,c) 1
-#endif
--- Assume we are using the newest versions when using ghci without cabal
-
 import Codec.TPTP.QuickCheck
 import Control.Applicative
 import Control.Monad
 import Control.Monad.Identity
-import Control.Monad.State
+import Control.Monad.Writer (Writer, runWriter)
 import Data.Data
 import Data.Function
 import Data.Monoid hiding(All)
@@ -30,14 +22,7 @@
 import Test.QuickCheck hiding ((.&.))
 import Data.Pointed
 import Data.Copointed
-#if !MIN_VERSION_transformers(0,4,0)
-import Control.Monad.Trans.Instances () -- Import Eq,Ord,Show,Read,Data,Typeable orphan instances for Data.Functor.Identity from transformers-compat package
-#endif
 
-#if !MIN_VERSION_base(4,7,0)
-import Util
-#endif
-
 -- * Basic undecorated formulae and terms
 
 -- | Basic (undecorated) first-order formulae
@@ -49,21 +34,21 @@
 -- * Formulae and terms decorated with state
 
 -- | First-order formulae decorated with state
-type FormulaST s = F (State s)
+type FormulaW s = F (Writer s)
 
 -- | Terms decorated with state
-type TermST s = T (State s)
+type TermW s = T (Writer s)
 
 -- | First-order formulae decorated with comments
-type FormulaC = FormulaST [String]
+type FormulaC = FormulaW [String]
 
 -- | Terms decorated with comments
-type TermC = TermST [String]
+type TermC = TermW [String]
 
 -- | Forget comments in formulae decorated with comments
 forgetFC :: FormulaC -> Formula
 forgetFC (F f) = F . return $
-  case evalState f [] of
+  case fst $ runWriter f of
     BinOp f1 op f2       -> BinOp (forgetFC f1) op (forgetFC f2)
     InfixPred t1 pred_ t2 -> InfixPred (forgetTC t1) pred_ (forgetTC t2)
     PredApp aw ts        -> PredApp aw (fmap forgetTC ts)
@@ -73,7 +58,7 @@
 -- | Forget comments in terms decorated with comments
 forgetTC :: TermC -> Term
 forgetTC (T t) = T . return $
-  case evalState t [] of
+  case fst $ runWriter t of
     Var v -> Var v
     NumberLitTerm d -> NumberLitTerm d
     DistinctObjectTerm s -> DistinctObjectTerm s
@@ -231,8 +216,8 @@
     deriving (Eq,Ord,Show,Read,Data,Typeable)
 -}
 
--- | A line of a TPTP file: Annotated formula (with the comment string embbeded in the State monad ), comment or include statement
-type TPTP_Input_C = TPTP_Input_ (State [String])
+-- | A line of a TPTP file: Annotated formula (with the comment string embbeded in the Writer monad ), comment or include statement
+type TPTP_Input_C = TPTP_Input_ (Writer [String])
 
 -- | Forget comments in a line of a TPTP file decorated with comments
 forgetTIC :: TPTP_Input_C -> TPTP_Input
@@ -258,15 +243,8 @@
 deriving instance Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c)
 deriving instance Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c)
 
-
-#if MIN_VERSION_base(4,7,0)
 deriving instance (Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c)
 deriving instance Typeable TPTP_Input_
-#else
-deriving instance (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c)
-instance Typeable1 c => Typeable (TPTP_Input_ c) where
-  typeOf = mkTypeOfForRank2Kind "Codec.TPTP.Base" "TPTP_Input_"
-#endif
 
 -- | Annotations about the formulas origin
 data Annotations = NoAnnotations | Annotations GTerm UsefulInfo
@@ -607,22 +585,11 @@
 DI(Show)
 DI(Read)
 
-#if MIN_VERSION_base(4,7,0)
 deriving instance Typeable F
 deriving instance Typeable T
 
 deriving instance (Typeable c, Data (c (Term0 (T c)))) => Data (T c)
 deriving instance (Typeable c, Data (c (Formula0 (T c) (F c)))) => Data (F c)
-#else
-instance Typeable1 c => Typeable (F c) where
-    typeOf = mkTypeOfForRank2Kind "Codec.TPTP.Base" "F"
-
-instance Typeable1 c => Typeable (T c) where
-    typeOf = mkTypeOfForRank2Kind "Codec.TPTP.Base" "T"
-
-deriving instance (Typeable1 c, Data (c (Term0 (T c)))) => Data (T c)
-deriving instance (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (F c)
-#endif
 
 -- * Utility functions
 
diff --git a/Codec/TPTP/Diff.hs b/Codec/TPTP/Diff.hs
--- a/Codec/TPTP/Diff.hs
+++ b/Codec/TPTP/Diff.hs
@@ -1,8 +1,8 @@
-{-# LANGUAGE CPP, NoMonomorphismRestriction, RecordWildCards
+{-# LANGUAGE NoMonomorphismRestriction, RecordWildCards
   , StandaloneDeriving, MultiParamTypeClasses, FunctionalDependencies
   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
-  , OverlappingInstances, OverloadedStrings, RankNTypes
+  , OverloadedStrings, RankNTypes
   #-}
 {-# OPTIONS -Wall #-}
 
@@ -11,19 +11,20 @@
 
 -- Warning: This module is a MESS (but it seems to work :)).
 
-#if MIN_VERSION_base(4,8,0)
 import Prelude hiding ((<$>))
-#endif
 
 import Data.Generics
 import Test.QuickCheck hiding((.&.))
 import Codec.TPTP.Base
 import Codec.TPTP.Pretty
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 import Control.Monad
 import Control.Monad.Identity
 
 
+text :: String -> Doc ann
+text = pretty
 
 
 data DiffResult d =
@@ -197,10 +198,10 @@
       _ -> let plug=plugSubformulae (T DontCare) (F DontCare) in Differ (plug f1) (plug f2)
 
 
-instance Show (T DiffResult) where
+instance {-# OVERLAPPING #-} Show (T DiffResult) where
     show (T t) = show t
 
-instance Show (F DiffResult) where
+instance {-# OVERLAPPING #-} Show (F DiffResult) where
     show (F f) = show f
 
 type T0Diff = DiffResult (Term0 (T DiffResult))
@@ -210,55 +211,55 @@
 wildcard :: AtomicWord
 wildcard = "_"
 
-instance Pretty (WithEnclosing T0Diff) where
-    pretty = prettyHelper --(plugSubterms (fApp wildcard []))
+instance PrettyAnsi (WithEnclosing T0Diff) where
+    prettyAnsi = prettyHelper --(plugSubterms (fApp wildcard []))
 
-instance Pretty (WithEnclosing F0Diff) where
-    pretty = prettyHelper --(plugSubformulae (fApp wildcard []) (pApp wildcard []))
+instance PrettyAnsi (WithEnclosing F0Diff) where
+    prettyAnsi = prettyHelper --(plugSubformulae (fApp wildcard []) (pApp wildcard []))
 
 prettyHelper :: forall t.
-                (Pretty (WithEnclosing t)) =>
-                WithEnclosing (DiffResult t) -> Doc
+                (PrettyAnsi (WithEnclosing t)) =>
+                WithEnclosing (DiffResult t) -> Doc AnsiStyle
 prettyHelper (WithEnclosing _ d) =
         let
-            pwe = pretty . WithEnclosing EnclNothing
+            pwe = prettyAnsi . WithEnclosing EnclNothing
         in
           case d of
-                 DontCare -> dullwhite.pretty $ wildcard
-                 Same -> dullgreen.text $ "Same"
-                 SameHead x -> blue . encloseSep (text "{ SameHead ") (text "}") semi $
+                 DontCare -> annotate (colorDull White).pretty $ wildcard
+                 Same -> annotate (colorDull Green).text $ "Same"
+                 SameHead x -> annotate (color Blue) . encloseSep (text "{ SameHead ") (text "}") semi $
                               [  pwe x
                               ]
 
 
 
-                 Differ x y -> red . encloseSep (text "{ Differ ") rbrace (text "; ") $
+                 Differ x y -> annotate (color Red) . encloseSep (text "{ Differ ") rbrace (text "; ") $
 
                               [ pwe x
                               , pwe y
                               ]
 
-deriving instance Pretty (T DiffResult)
+deriving instance PrettyAnsi (T DiffResult)
 
-deriving instance Pretty (F DiffResult)
+deriving instance PrettyAnsi (F DiffResult)
 
-instance Pretty (WithEnclosing (T DiffResult)) where
-    pretty (WithEnclosing x (T y)) = pretty (WithEnclosing x y)
+instance PrettyAnsi (WithEnclosing (T DiffResult)) where
+    prettyAnsi (WithEnclosing x (T y)) = prettyAnsi (WithEnclosing x y)
 
-instance Pretty (WithEnclosing (F DiffResult)) where
-    pretty (WithEnclosing x (F y)) = pretty (WithEnclosing x y)
+instance PrettyAnsi (WithEnclosing (F DiffResult)) where
+    prettyAnsi (WithEnclosing x (F y)) = prettyAnsi (WithEnclosing x y)
 
-instance Pretty (T0Diff) where
-    pretty = pretty . WithEnclosing EnclNothing
+instance PrettyAnsi (T0Diff) where
+    prettyAnsi = prettyAnsi . WithEnclosing EnclNothing
 
-instance Pretty (F0Diff) where
-    pretty = pretty . WithEnclosing EnclNothing
+instance PrettyAnsi (F0Diff) where
+    prettyAnsi = prettyAnsi . WithEnclosing EnclNothing
 
--- instance Pretty (DiffResult (T DiffResult)) where
---     pretty = pretty . WithEnclosing EnclNothing . T
+-- instance PrettyAnsi (DiffResult (T DiffResult)) where
+--     prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . T
 
--- instance Pretty (DiffResult (T DiffResult) (F DiffResult)) where
---     pretty = pretty . WithEnclosing EnclNothing . F
+-- instance PrettyAnsi (DiffResult (T DiffResult) (F DiffResult)) where
+--     prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . F
 
 
 -- runFormulaDiff :: Formula
@@ -300,12 +301,14 @@
   xs <- sample' diffGenF
   ys <- sample' diffGenF
 
-  let item x y = text (replicate 50 '=')
-                 <$> pretty x
-                 <$> text (replicate 40 '-')
-                 <$> pretty y
-                 <$> text (replicate 40 '-')
-                 <$> pretty (diffFormula x y)
+  let item x y = vsep
+                 [ text (replicate 50 '=')
+                 , prettyAnsi x
+                 , text (replicate 40 '-')
+                 , prettyAnsi y
+                 , text (replicate 40 '-')
+                 , prettyAnsi (diffFormula x y)
+                 ]
 
   mapM_ (putStrLn . prettySimple . uncurry item) (zip xs ys)
 
diff --git a/Codec/TPTP/Export.hs b/Codec/TPTP/Export.hs
--- a/Codec/TPTP/Export.hs
+++ b/Codec/TPTP/Export.hs
@@ -2,7 +2,7 @@
   , StandaloneDeriving
   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
-  , OverlappingInstances, RankNTypes
+  , RankNTypes
   #-}
 {-# OPTIONS -Wall #-}
 module Codec.TPTP.Export(toTPTP',ToTPTP(..),isLowerWord) where
diff --git a/Codec/TPTP/Pretty.hs b/Codec/TPTP/Pretty.hs
--- a/Codec/TPTP/Pretty.hs
+++ b/Codec/TPTP/Pretty.hs
@@ -1,49 +1,63 @@
-{-# LANGUAGE CPP, NoMonomorphismRestriction, RecordWildCards
+{-# LANGUAGE NoMonomorphismRestriction, RecordWildCards
   , StandaloneDeriving
   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
-  , OverlappingInstances, RankNTypes, PatternGuards
+  , RankNTypes, PatternGuards
   #-}
 
 {-# OPTIONS -Wall -fno-warn-orphans #-}
 
 -- | Mainly just 'Pretty' instances
-module Codec.TPTP.Pretty(prettySimple,WithEnclosing(..),Enclosing(..)) where
+module Codec.TPTP.Pretty(PrettyAnsi(..),prettySimple,WithEnclosing(..),Enclosing(..)) where
 
-#if MIN_VERSION_base(4,8,0)
 import Prelude hiding ((<$>))
-#endif
 
 import Codec.TPTP.Base
 import Codec.TPTP.Export
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 import Data.Data
 import Control.Monad.Identity
 import Data.Ratio
+import qualified Data.Text.Lazy as TL
 
-oper :: String -> Doc
-oper = dullyellow . text
-psym :: forall a. (Pretty a) => a -> Doc
-psym = green . pretty
-fsym :: forall a. (Pretty a) => a -> Doc
-fsym = yellow . pretty
+class PrettyAnsi a where
+  prettyAnsi :: a -> Doc AnsiStyle
+  prettyAnsiList :: [a] -> Doc AnsiStyle
+  prettyAnsiList = align . list . map prettyAnsi
 
+instance PrettyAnsi (Doc AnsiStyle) where
+  prettyAnsi = id
+
+instance PrettyAnsi a => PrettyAnsi [a] where
+  prettyAnsi = prettyAnsiList
+
+oper :: String -> Doc AnsiStyle
+oper = annotate (colorDull Yellow) . text
+psym :: forall a. (Pretty a) => a -> Doc AnsiStyle
+psym = annotate (color Green) . pretty
+fsym :: forall a. (Pretty a) => a -> Doc AnsiStyle
+fsym = annotate (color Yellow) . pretty
+
+text :: String -> Doc ann
+text = pretty
+
 --wtext :: String -> Doc
---wtext = white . text
+--wtext = annotate (color White) . text
 
-prettyargs :: forall a. (Pretty a) => [a] -> Doc
+prettyargs :: forall a. (PrettyAnsi a) => [a] -> Doc AnsiStyle
 --prettyargs = encloseSep (wtext "(") (wtext ")") (wtext ",") . fmap pretty
-prettyargs = tupled . fmap pretty
--- prettyargs [] = white $ text "()"
+prettyargs = tupled . fmap prettyAnsi
+-- prettyargs [] = annotate (color White) $ text "()"
 -- prettyargs (x:xs) =
---     let pxs = fmap ((white (text ",") <+>) . pretty) xs in
+--     let pxs = fmap ((annotate (color White) (text ",") <+>) . pretty) xs in
 
---     align (fillSep $ [    white (text "(") <+> pretty x ]
+--     align (fillSep $ [    annotate (color White) (text "(") <+> pretty x ]
 --                     ++ pxs
---                     ++ [ white (text ")") ] )
+--                     ++ [ annotate (color White) (text ")") ] )
 
-prational :: Rational -> Doc
-prational q = (text.show.numerator) q <> char '/' <> (text.show.denominator) q
+prational :: Rational -> Doc ann
+prational q = (text.show.numerator) q <> pretty '/' <> (text.show.denominator) q
 
 -- | Carries information about the enclosing operation (for the purpose of printing stuff without parentheses if possible).
 data WithEnclosing a = WithEnclosing Enclosing a
@@ -87,36 +101,37 @@
                EnclNothing -> (-1000) -- if there's no enclosing operation, we don't need parentheses
 
 
-maybeParens :: Enclosing -> Enclosing -> Doc -> Doc
+maybeParens :: Enclosing -> Enclosing -> Doc ann -> Doc ann
 maybeParens inner outer | needsParens inner outer = parens
 maybeParens _ _ = id
 
-instance Pretty TPTP_Input where
-    pretty AFormula{..}
-        = (text) "Formula " <+> (dullwhite.text) "name:"
-          </>
-          vsep
-          [
-            (red.pretty) name <+> dullwhite (text "role:") <+> (magenta.text.unrole) role
-          , pretty formula
-          , pretty annotations
-          ,empty
+instance PrettyAnsi TPTP_Input where
+    prettyAnsi AFormula{..}
+        = fillSep
+          [ (text) "Formula " <+> (annotate (colorDull White).text) "name:"
+          , vsep
+            [
+              (annotate (color Red).pretty) name <+> annotate (colorDull White) (text "role:") <+> (annotate (color Magenta).text.unrole) role
+            , prettyAnsi formula
+            , prettyAnsi annotations
+            , mempty
+            ]
           ]
 
-    pretty (Comment str)
-        = magenta . string $ str
+    prettyAnsi (Comment str)
+        = annotate (color Magenta) . pretty $ str
 
-    pretty (Include f sel) = text "include" <> parens (squotes (text f) <> (case sel of { [] -> empty; _ -> comma <+> sep (punctuate comma (fmap pretty sel)) } ))
+    prettyAnsi (Include f sel) = text "include" <> parens (squotes (text f) <> (case sel of { [] -> mempty; _ -> comma <+> sep (punctuate comma (fmap pretty sel)) } ))
 
 
-    prettyList = foldr (\x xs -> pretty x <$> xs) empty
+    prettyAnsiList = foldr (\x xs -> vsep [prettyAnsi x, xs]) mempty
 
-instance Pretty Quant where
-    pretty All = oper "∀"
-    pretty Exists = oper "∃"
+instance PrettyAnsi Quant where
+    prettyAnsi All = oper "∀"
+    prettyAnsi Exists = oper "∃"
 
-instance (Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty ((WithEnclosing (Formula0 t f))) where
-    pretty (WithEnclosing enclosing formu) =
+instance (PrettyAnsi (WithEnclosing t), PrettyAnsi (WithEnclosing f)) => PrettyAnsi ((WithEnclosing (Formula0 t f))) where
+    prettyAnsi (WithEnclosing enclosing formu) =
         let
             newEnclosing =
              case formu of
@@ -134,25 +149,27 @@
           case formu of
 
             Quant q vars f ->
-               pretty q
-               <+> brackets (hsep (punctuate comma (fmap pretty vars)))
-               <> dot
-               </> pretty (wne f)
+               fillSep
+               [ prettyAnsi q
+                 <+> brackets (hsep (punctuate comma (fmap prettyAnsi vars)))
+                 <> dot
+               , prettyAnsi (wne f)
+               ]
 
-            (:~:) f -> oper "¬" <+> pretty (wne f)
+            (:~:) f -> oper "¬" <+> prettyAnsi (wne f)
 
             PredApp p [] -> psym p
             PredApp p args -> psym p <> prettyargs (fmap wne args)
 
 
             BinOp f1 op f2 ->
-                align $ sep [indent 0 $ pretty (wne f1), pretty op, indent 0 $ pretty (wne f2)]
+                align $ sep [indent 0 $ prettyAnsi (wne f1), prettyAnsi op, indent 0 $ prettyAnsi (wne f2)]
 
             InfixPred f1 op f2 ->
-                align $ sep [indent 0 $ pretty (wne f1), pretty op, indent 0 $ pretty (wne f2)]
+                align $ sep [indent 0 $ prettyAnsi (wne f1), prettyAnsi op, indent 0 $ prettyAnsi (wne f2)]
 
-instance Pretty BinOp where
-    pretty x = case x of
+instance PrettyAnsi BinOp where
+    prettyAnsi x = case x of
         (:<=>:) -> oper "⇔"
         (:=>:)  -> oper "⇒"
         (:<=:)  -> oper "⇐"
@@ -162,78 +179,79 @@
         (:~|:)  -> oper "NOR"
         (:<~>:) -> oper "XOR"
 
-instance Pretty InfixPred where
-    pretty x = case x of
+instance PrettyAnsi InfixPred where
+    prettyAnsi x = case x of
         (:=:)   -> oper "="
         (:!=:)  -> oper "≠"
 
-instance (Pretty (WithEnclosing t)) => Pretty (WithEnclosing (Term0 t)) where
-    pretty (WithEnclosing _ x) =
+instance (PrettyAnsi (WithEnclosing t)) => PrettyAnsi (WithEnclosing (Term0 t)) where
+    prettyAnsi (WithEnclosing _ x) =
         case x of
-          Var s -> pretty s
+          Var s -> prettyAnsi s
           NumberLitTerm d -> prational d
-          DistinctObjectTerm s -> cyan (dquotes (text s))
+          DistinctObjectTerm s -> annotate (color Cyan) (dquotes (text s))
           FunApp f [] -> fsym f
           FunApp f args -> fsym f <> prettyargs (fmap (WithEnclosing EnclNothing) args)
 
 
 
-instance Pretty (Formula0 Term Formula) where
-    pretty = pretty . WithEnclosing EnclNothing . F . Identity
+instance PrettyAnsi (Formula0 Term Formula) where
+    prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . F . Identity
 
-instance Pretty (Term0 Term) where
-    pretty = pretty . WithEnclosing EnclNothing . T . Identity
+instance PrettyAnsi (Term0 Term) where
+    prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . T . Identity
 
-instance Pretty (WithEnclosing Formula) where
-    pretty (WithEnclosing x (F (Identity y))) = pretty (WithEnclosing x y)
+instance PrettyAnsi (WithEnclosing Formula) where
+    prettyAnsi (WithEnclosing x (F (Identity y))) = prettyAnsi (WithEnclosing x y)
 
-instance Pretty (WithEnclosing Term) where
-    pretty (WithEnclosing x (T (Identity y))) = pretty (WithEnclosing x y)
+instance PrettyAnsi (WithEnclosing Term) where
+    prettyAnsi (WithEnclosing x (T (Identity y))) = prettyAnsi (WithEnclosing x y)
 
-deriving instance Pretty Formula
-deriving instance Pretty Term
-deriving instance Pretty a => Pretty (Identity a)
+deriving instance PrettyAnsi Formula
+deriving instance PrettyAnsi Term
+deriving instance PrettyAnsi a => PrettyAnsi (Identity a)
 
--- instance (Pretty f, Pretty t) => Pretty (Formula0 t f) where
+-- instance (Pretty f, Pretty t) => PrettyAnsi (Formula0 t f) where
 --     pretty = pretty . WithEnclosing ""
 
 -- instance (Pretty t) => Pretty (Term0 t) where
 --     pretty = pretty . WithEnclosing ""
 
-prettySimple :: Pretty a => a -> String
-prettySimple x = displayS (renderPretty 0.9 80 (pretty x)) ""
+prettySimple :: PrettyAnsi a => a -> String
+prettySimple x = TL.unpack $ renderLazy $ layoutSmart LayoutOptions{ layoutPageWidth = AvailablePerLine 80 0.9 } $ prettyAnsi x
 
-instance Pretty Annotations where
-    pretty NoAnnotations = dullwhite . text $ "NoAnnotations"
-    pretty (Annotations a b) = dullwhite (text "SourceInfo: ") <+> pretty a <+> pretty b
 
-instance Pretty UsefulInfo where
-    pretty NoUsefulInfo = empty
-    pretty (UsefulInfo x) = dullwhite (text "UsefulInfo: ") <+> pretty x
+instance PrettyAnsi Annotations where
+    prettyAnsi NoAnnotations = annotate (colorDull White) . text $ "NoAnnotations"
+    prettyAnsi (Annotations a b) = annotate (colorDull White) (text "SourceInfo: ") <+> prettyAnsi a <+> prettyAnsi b
 
+instance PrettyAnsi UsefulInfo where
+    prettyAnsi NoUsefulInfo = mempty
+    prettyAnsi (UsefulInfo x) = annotate (colorDull White) (text "UsefulInfo: ") <+> prettyAnsi x
 
 
-instance Pretty GData where
-    pretty (GWord x) = pretty x
-    pretty (GNumber x) = prational x
-    pretty (GDistinctObject x) = cyan (dquotes (text x))
-    pretty (GApp x []) = fsym x
-    pretty (GApp x args) = fsym x <+> prettyargs args
-    pretty (GFormulaData s f) = text s <> align (parens (pretty f))
-    pretty (GFormulaTerm s t) = text s <> align (parens (pretty t))
-    pretty (GVar x) = pretty x
 
+instance PrettyAnsi GData where
+    prettyAnsi (GWord x) = pretty x
+    prettyAnsi (GNumber x) = prational x
+    prettyAnsi (GDistinctObject x) = annotate (color Cyan) (dquotes (text x))
+    prettyAnsi (GApp x []) = fsym x
+    prettyAnsi (GApp x args) = fsym x <+> prettyargs args
+    prettyAnsi (GFormulaData s f) = text s <> align (parens (prettyAnsi f))
+    prettyAnsi (GFormulaTerm s t) = text s <> align (parens (prettyAnsi t))
+    prettyAnsi (GVar x) = prettyAnsi x
+
 instance Pretty AtomicWord where
     pretty (AtomicWord x) = (if isLowerWord x then text else squotes.text) x
 
-instance Pretty GTerm where
-    pretty (GTerm x) = pretty x
-    pretty (ColonSep x y) = pretty x <+> oper ":" <+> pretty y
-    pretty (GList xs) = let f = oper
-                        in
-                          f "[" <+> (fillSep . punctuate comma . fmap pretty) xs <+> f "]"
+instance PrettyAnsi GTerm where
+    prettyAnsi (GTerm x) = prettyAnsi x
+    prettyAnsi (ColonSep x y) = prettyAnsi x <+> oper ":" <+> prettyAnsi y
+    prettyAnsi (GList xs) = let f = oper
+                            in
+                              f "[" <+> (fillSep . punctuate comma . fmap prettyAnsi) xs <+> f "]"
 
 
 
-instance Pretty V where
-    pretty (V x) = blue . text $ x
+instance PrettyAnsi V where
+    prettyAnsi (V x) = annotate (color Blue) . text $ x
diff --git a/Codec/TPTP/QuickCheck.hs b/Codec/TPTP/QuickCheck.hs
--- a/Codec/TPTP/QuickCheck.hs
+++ b/Codec/TPTP/QuickCheck.hs
@@ -2,14 +2,13 @@
   , StandaloneDeriving
   , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
   , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
-  , OverlappingInstances, RankNTypes, PatternGuards
+  , RankNTypes, PatternGuards
   #-}
 {-# OPTIONS -Wall #-}
 module Codec.TPTP.QuickCheck where
 
 import Test.QuickCheck
 import Control.Monad
-import Control.Applicative
 import Data.Char
 import Data.Array.ST
 import Data.Array.IArray
diff --git a/ParserC.y b/ParserC.y
--- a/ParserC.y
+++ b/ParserC.y
@@ -12,7 +12,7 @@
 import System.IO
 import System.IO.Unsafe
 import Control.Monad.Identity
-import Control.Monad.State
+import Control.Monad.Writer
 }
 
 %name parseTPTPwithComment
@@ -505,8 +505,8 @@
 instance Commented Identity where
   withComments = const
 
-instance Commented (State [String]) where
-  withComments (F mf) s = F $ do { f <- mf; put s; return f }
+instance Commented (Writer [String]) where
+  withComments (F mf) s = F $ do { f <- mf; tell s; return f }
 
 
 stripQuotes which (x:xs) = go xs
diff --git a/Util.hs b/Util.hs
--- a/Util.hs
+++ b/Util.hs
@@ -6,26 +6,3 @@
 #ifndef MIN_VERSION_base
 #define MIN_VERSION_base(X,Y,Z) 1
 #endif
-
-#if !MIN_VERSION_base(4,7,0)
-import Data.Typeable
-
-#if ! MIN_VERSION_base(4,4,0)
-mkTyCon3 _ m t = mkTyCon $ m++"."++t
-#endif
-
-packageName :: String
-packageName = "logic-TPTP"
-
-
--- | Gets the TypeRep of @c@ (not of @c ()@)
-getTyRep1 :: forall c. Typeable1 c => c () -> TypeRep
-getTyRep1 _ = mkTyConApp (typeRepTyCon (typeOf1 (undefined :: c ()))) []
-
-
-mkTypeOfForRank2Kind :: forall x c. Typeable1 c => String -> String -> x c -> TypeRep
-mkTypeOfForRank2Kind moduleName typeName = const tr
-    where
-        tc = mkTyCon3 packageName moduleName typeName
-        tr = mkTyConApp tc [getTyRep1 (undefined :: c ())]
-#endif
diff --git a/changelog.markdown b/changelog.markdown
--- a/changelog.markdown
+++ b/changelog.markdown
@@ -1,3 +1,8 @@
+## 0.6.0.0
+
+* Migrate to `prettyprinter` package family from `ansi-wl-pprint` package
+* Use `Writer` moand instead of `State` to annotate comments
+
 ## 0.5.1.0
 
 * Fix compilation error with `mtl >=2.3`
diff --git a/logic-TPTP.cabal b/logic-TPTP.cabal
--- a/logic-TPTP.cabal
+++ b/logic-TPTP.cabal
@@ -1,5 +1,5 @@
 name: logic-TPTP
-version: 0.5.1.0
+version: 0.6.0.0
 cabal-version: >= 1.10
 build-type: Simple
 license: GPL
@@ -8,7 +8,7 @@
 bug-reports: http://github.com/DanielSchuessler/logic-TPTP/issues
 synopsis: Import, export etc. for TPTP, a syntax for first-order logic
 description:
- For information about the TPTP format, see <http://www.cs.miami.edu/~tptp/>.
+ For information about the TPTP format, see <https://www.tptp.org/>.
  .
  Components:
  .
@@ -60,17 +60,18 @@
 Library
  ghc-options: -Wall -O2
 
- build-depends:      base >=4 && < 5
+ build-depends:      base >=4.8.0.0 && < 5
                    , array
                    , syb
                    , containers
-                   , ansi-wl-pprint < 1.0
+                   , prettyprinter >=1.2.1.1 && <1.8
+                   , prettyprinter-ansi-terminal >=1.0 && <1.2
+                   , text
                    , QuickCheck >= 2
                    , mtl
                    , pointed
                    , semigroups
-                   , transformers
-                   , transformers-compat >= 0.5
+                   , transformers >= 0.5
 
  exposed-modules:   Codec.TPTP.Import
                   , Codec.TPTP.Base
@@ -97,12 +98,11 @@
  hs-source-dirs:    testing
  build-depends:     logic-TPTP
                   , base
-                  , ansi-wl-pprint
+                  , prettyprinter
+                  , prettyprinter-ansi-terminal
                   , optparse-applicative >=0.11 && <0.19
                   , pcre-light
                   , semigroups
- if impl(ghc <7.10)
-  build-depends:    pcre-light <0.4.1
  default-language:  Haskell2010
  other-extensions:  CPP
  if !flag(BuildTestPrograms)
@@ -115,14 +115,12 @@
  hs-source-dirs:    testing
  build-depends:     logic-TPTP
                   , base
-                  , ansi-wl-pprint
+                  , prettyprinter
+                  , prettyprinter-ansi-terminal
                   , pcre-light
                   , QuickCheck
                   , semigroups
                   , transformers
-                  , transformers-compat >= 0.5
- if impl(ghc <7.10)
-  build-depends:    pcre-light <0.4.1
  default-language:  Haskell2010
  other-extensions:  CPP
 
@@ -132,7 +130,8 @@
                   , SimpleArgs
  hs-source-dirs:    testing
  build-depends:     logic-TPTP
-                  , ansi-wl-pprint
+                  , prettyprinter
+                  , prettyprinter-ansi-terminal
                   , base
                   , bytestring
                   , containers
@@ -142,8 +141,6 @@
                   , QuickCheck
                   , semigroups
                   , syb
- if impl(ghc <7.10)
-  build-depends:    pcre-light <0.4.1
  default-language:  Haskell2010
  other-extensions:  CPP
  if !flag(BuildTestPrograms)
@@ -155,7 +152,8 @@
                   , SimpleArgs
  hs-source-dirs:    testing
  build-depends:     logic-TPTP
-                  , ansi-wl-pprint
+                  , prettyprinter
+                  , prettyprinter-ansi-terminal
                   , base
                   , bytestring
                   , containers
@@ -165,8 +163,6 @@
                   , QuickCheck
                   , semigroups
                   , syb
- if impl(ghc <7.10)
-  build-depends:    pcre-light <0.4.1
  default-language:  Haskell2010
  other-extensions:  CPP
  if !flag(BuildTestPrograms)
diff --git a/testing/Common.hs b/testing/Common.hs
--- a/testing/Common.hs
+++ b/testing/Common.hs
@@ -4,9 +4,9 @@
 
 module Common where
 
-import Data.Monoid
 import qualified Data.Semigroup as Semigroup
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 import Text.Regex.PCRE.Light.Char8
 import Codec.TPTP
 
@@ -28,14 +28,14 @@
     mappend = (Semigroup.<>)
 #endif
 
-instance Pretty AFormulaComparison where
-    pretty (OtherSame) = dullgreen.text$"OtherSame"
-    pretty (OtherDiff x y) = sep
-                             [dullred.text$"OtherDiff"
+instance PrettyAnsi AFormulaComparison where
+    prettyAnsi (OtherSame) = annotate (colorDull Green).pretty$"OtherSame"
+    prettyAnsi (OtherDiff x y) = sep
+                             [annotate (colorDull Red).pretty$"OtherDiff"
                              ,pretty x
                              ,pretty y
                              ]
-    pretty (FormulaDiff fd) = pretty fd
+    prettyAnsi (FormulaDiff fd) = prettyAnsi fd
 
 compareOther ::  (Eq a, Show a) => a -> a -> AFormulaComparison
 compareOther x y = if x==y then OtherSame else OtherDiff (show x) (show y)
diff --git a/testing/ParseRandom.hs b/testing/ParseRandom.hs
--- a/testing/ParseRandom.hs
+++ b/testing/ParseRandom.hs
@@ -18,7 +18,6 @@
 import Data.Generics
 import Test.QuickCheck
 import Data.Monoid
-import Text.PrettyPrint.ANSI.Leijen
 import System.Exit
 import Text.Regex.PCRE.Light.Char8
 import Common
diff --git a/testing/PrettyPrintFile.hs b/testing/PrettyPrintFile.hs
--- a/testing/PrettyPrintFile.hs
+++ b/testing/PrettyPrintFile.hs
@@ -19,7 +19,6 @@
 import Data.Generics
 import Test.QuickCheck
 import Data.Monoid
-import Text.PrettyPrint.ANSI.Leijen
 import System.Exit
 import Text.Regex.PCRE.Light.Char8
 
diff --git a/testing/SimpleArgs.hs b/testing/SimpleArgs.hs
--- a/testing/SimpleArgs.hs
+++ b/testing/SimpleArgs.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-}
+{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
 
 -- Copied and modified from https://hackage.haskell.org/package/simpleargs-0.2.1
 -- which is licensed under GNU LESSER GENERAL PUBLIC LICENSE Version 2.1
diff --git a/testing/TestImportExportImportFile.hs b/testing/TestImportExportImportFile.hs
--- a/testing/TestImportExportImportFile.hs
+++ b/testing/TestImportExportImportFile.hs
@@ -3,7 +3,8 @@
 
 import Control.Monad
 import Data.Monoid
-import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import Prettyprinter
+import Prettyprinter.Render.Terminal
 import System.Exit
 import Common
 import Options.Applicative
@@ -49,7 +50,7 @@
   case findUnsupportedFormulaType input of
      Just x -> do
        unless print_failure_only $ 
-         putStrLn . prettySimple . yellow . text $ ("Skipping unsupported formula type "++x)
+         putStrLn . prettySimple . annotate (color Yellow) . text $ ("Skipping unsupported formula type "++x)
      Nothing -> do
 
       let once = parse input
@@ -58,7 +59,7 @@
         putStrLn $ "new tptp = " ++tptp
       let twice = parse tptp
       let dif = mconcat (zipWith diffAFormula once twice)
-      let success = (putStrLn . prettySimple . dullgreen . text $ "Ok")
+      let success = (putStrLn . prettySimple . annotate (colorDull Green) . text $ "Ok")
 
       -- case dif of
       --   OtherSame -> success
@@ -74,3 +75,6 @@
            when print_failure_only $ putStrLn infilename'
            putStrLn . prettySimple $ dif
            exitWith (ExitFailure 1)
+
+text :: String -> Doc ann
+text = pretty