diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,17 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [0.3.1.0] -- 2023-07-19
+
+### Added
+- Added support to `Data.Text`. ([#95](https://github.com/lsrcz/grisette/pull/95))
+- Added `Arbitrary` instances for bit vectors. ([#97](https://github.com/lsrcz/grisette/pull/97))
+- Added pretty printers for Grisette data types. ([#101](https://github.com/lsrcz/grisette/pull/101))
+- Added `ExtractSymbolics` instances for tuples longer than 2. ([#103](https://github.com/lsrcz/grisette/pull/103))
+
+### Fixed
+- Fixed the `Read` instance for bit vectors. ([#99](https://github.com/lsrcz/grisette/pull/99), [#100](https://github.com/lsrcz/grisette/pull/100))
+
 ## [0.3.0.0] -- 2023-07-07
 
 ### Added
@@ -52,6 +63,10 @@
 ### Added
 - Initial release for Grisette.
 
+[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...HEAD
+[0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0
+[0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0
+[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...HEAD
 [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0
 [0.2.0.0]: https://github.com/lsrcz/grisette/compare/v0.1.0.0...v0.2.0.0
 [0.1.0.0]: https://github.com/lsrcz/grisette/tree/v0.1.0.0
diff --git a/grisette.cabal b/grisette.cabal
--- a/grisette.cabal
+++ b/grisette.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           grisette
-version:        0.3.0.0
+version:        0.3.1.0
 synopsis:       Symbolic evaluation as a library
 description:    Grisette is a reusable symbolic evaluation library for Haskell. By
                 translating programs into constraints, Grisette can help the development of
@@ -16,8 +16,8 @@
                 .
                 For more details, please checkout the README.
 category:       Formal Methods, Theorem Provers, Symbolic Computation, SMT
-homepage:       https://github.com/lsrcz/grisette-haskell#readme
-bug-reports:    https://github.com/lsrcz/grisette-haskell/issues
+homepage:       https://github.com/lsrcz/grisette#readme
+bug-reports:    https://github.com/lsrcz/grisette/issues
 author:         Sirui Lu, Rastislav Bodík
 maintainer:     Sirui Lu (siruilu@cs.washington.edu)
 copyright:      2021-2023 Sirui Lu
@@ -36,7 +36,7 @@
 
 source-repository head
   type: git
-  location: https://github.com/lsrcz/grisette-haskell
+  location: https://github.com/lsrcz/grisette
 
 flag fast
   description: Compile with O2 optimization
@@ -66,6 +66,7 @@
       Grisette.Core.Data.Class.ExtractSymbolics
       Grisette.Core.Data.Class.Function
       Grisette.Core.Data.Class.GenSym
+      Grisette.Core.Data.Class.GPretty
       Grisette.Core.Data.Class.Mergeable
       Grisette.Core.Data.Class.ModelOps
       Grisette.Core.Data.Class.SafeArith
@@ -126,7 +127,8 @@
   hs-source-dirs:
       src
   build-depends:
-      array >=0.5.4 && <0.6
+      QuickCheck >=2.13.2 && <2.15
+    , array >=0.5.4 && <0.6
     , base >=4.14 && <5
     , bytestring >=0.10.12 && <0.12
     , call-stack >=0.1 && <0.5
@@ -138,8 +140,10 @@
     , loch-th >=0.2.2 && <0.3
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
+    , prettyprinter >=1.5.0 && <1.8
     , sbv >=8.11 && <10.3
     , template-haskell >=2.16 && <2.21
+    , text >=1.2.4.1 && <2.1
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
@@ -159,6 +163,7 @@
       doctest
   build-depends:
       Glob
+    , QuickCheck >=2.13.2 && <2.15
     , array >=0.5.4 && <0.6
     , base >=4.14 && <5
     , bytestring >=0.10.12 && <0.12
@@ -173,8 +178,10 @@
     , loch-th >=0.2.2 && <0.3
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
+    , prettyprinter >=1.5.0 && <1.8
     , sbv >=8.11 && <10.3
     , template-haskell >=2.16 && <2.21
+    , text >=1.2.4.1 && <2.1
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
@@ -195,6 +202,7 @@
       Grisette.Backend.SBV.Data.SMT.TermRewritingTests
       Grisette.Core.Control.Monad.UnionMTests
       Grisette.Core.Data.BVTests
+      Grisette.Core.Data.Class.GPrettyTests
       Grisette.IR.SymPrim.Data.Prim.BitsTests
       Grisette.IR.SymPrim.Data.Prim.BoolTests
       Grisette.IR.SymPrim.Data.Prim.BVTests
@@ -208,7 +216,8 @@
   hs-source-dirs:
       test
   build-depends:
-      array >=0.5.4 && <0.6
+      QuickCheck >=2.13.2 && <2.15
+    , array >=0.5.4 && <0.6
     , base >=4.14 && <5
     , bytestring >=0.10.12 && <0.12
     , call-stack >=0.1 && <0.5
@@ -221,12 +230,14 @@
     , loch-th >=0.2.2 && <0.3
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
+    , prettyprinter >=1.5.0 && <1.8
     , sbv >=8.11 && <10.3
     , tasty >=1.1.0.3 && <1.5
     , tasty-hunit ==0.10.*
     , tasty-quickcheck >=0.10.1 && <0.11
     , tasty-test-reporter >=0.1.1.2 && <0.2
     , template-haskell >=2.16 && <2.21
+    , text >=1.2.4.1 && <2.1
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.7
     , unordered-containers >=0.2.11 && <0.3
diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs
--- a/src/Grisette/Core.hs
+++ b/src/Grisette/Core.hs
@@ -613,6 +613,9 @@
     ToCon (..),
     ToSym (..),
 
+    -- * Pretty printing
+    GPretty (..),
+
     -- * Symbolic Generation
 
     -- | It is usually useful to generate complex symbolic values. For example,
@@ -1020,6 +1023,7 @@
 import Grisette.Core.Data.Class.Evaluate
 import Grisette.Core.Data.Class.ExtractSymbolics
 import Grisette.Core.Data.Class.Function
+import Grisette.Core.Data.Class.GPretty
 import Grisette.Core.Data.Class.GenSym
 import Grisette.Core.Data.Class.Mergeable
 import Grisette.Core.Data.Class.ModelOps
diff --git a/src/Grisette/Core/Control/Monad/UnionM.hs b/src/Grisette/Core/Control/Monad/UnionM.hs
--- a/src/Grisette/Core/Control/Monad/UnionM.hs
+++ b/src/Grisette/Core/Control/Monad/UnionM.hs
@@ -7,6 +7,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskellQuotes #-}
 {-# LANGUAGE Trustworthy #-}
@@ -55,6 +56,7 @@
 import Grisette.Core.Data.Class.Evaluate
 import Grisette.Core.Data.Class.ExtractSymbolics
 import Grisette.Core.Data.Class.Function
+import Grisette.Core.Data.Class.GPretty
 import Grisette.Core.Data.Class.GenSym
 import Grisette.Core.Data.Class.Mergeable
 import Grisette.Core.Data.Class.SOrd
@@ -71,6 +73,12 @@
 import Language.Haskell.TH.Syntax
 import Language.Haskell.TH.Syntax.Compat (unTypeSplice)
 
+#if MIN_VERSION_prettyprinter(1,7,0)
+import Prettyprinter
+#else
+import Data.Text.Prettyprint.Doc
+#endif
+
 -- $setup
 -- >>> import Grisette.Core
 -- >>> import Grisette.IR.SymPrim
@@ -238,6 +246,11 @@
     wrapBracket '{' '}'
       . liftShowsPrecUnion sp sl 0
       $ a
+
+instance (GPretty a) => GPretty (UnionM a) where
+  gpretty = \case
+    (UAny a) -> groupedEnclose "<" ">" $ gpretty a
+    (UMrg _ a) -> groupedEnclose "{" "}" $ gpretty a
 
 -- | Extract the underlying Union. May be unmerged.
 underlyingUnion :: UnionM a -> Union a
diff --git a/src/Grisette/Core/Data/BV.hs b/src/Grisette/Core/Data/BV.hs
--- a/src/Grisette/Core/Data/BV.hs
+++ b/src/Grisette/Core/Data/BV.hs
@@ -44,11 +44,13 @@
   )
 where
 
+import Control.Applicative
 import Control.DeepSeq
 import Control.Exception
 import Data.Bits
 import Data.CallStack
 import Data.Hashable
+import Data.Maybe
 import Data.Proxy
 import Data.Typeable
 import GHC.Enum
@@ -60,6 +62,9 @@
 import Grisette.Utils.Parameterized
 import Language.Haskell.TH.Syntax
 import Numeric
+import qualified Test.QuickCheck as QC
+import Text.ParserCombinators.ReadP (skipSpaces, string)
+import Text.ParserCombinators.ReadPrec
 import Text.Read
 import qualified Text.Read.Lex as L
 
@@ -161,8 +166,26 @@
   | Just i <- L.numberToInteger n = return (fromInteger i)
 convertInt _ = pfail
 
+readBinary :: (Num a) => ReadPrec a
+readBinary = parens $ do
+  r0 <- look
+  case r0 of
+    ('-' : _) -> do
+      _ <- get
+      negate <$> parens parse0b
+    _ -> parse0b
+  where
+    isDigit c = isJust (valDig c)
+    valDigit c = fromMaybe 0 (valDig c)
+    valDig '0' = Just 0
+    valDig '1' = Just 1
+    valDig _ = Nothing
+    parse0b = do
+      _ <- Text.Read.lift $ string "0b"
+      fromInteger <$> Text.Read.lift (L.readIntP 2 isDigit valDigit)
+
 instance (KnownNat n, 1 <= n) => Read (WordN n) where
-  readPrec = readNumber convertInt
+  readPrec = readNumber convertInt <|> readBinary
   readListPrec = readListPrecDefault
   readList = readListDefault
 
@@ -257,7 +280,7 @@
       binRep = showIntAtBase 2 (\x -> if x == 0 then '0' else '1') w ""
 
 instance (KnownNat n, 1 <= n) => Read (IntN n) where
-  readPrec = readNumber convertInt
+  readPrec = readNumber convertInt <|> readBinary
   readListPrec = readListPrecDefault
   readList = readListDefault
 
@@ -417,6 +440,10 @@
   signum = unarySomeWordNR1 signum
   fromInteger = error "fromInteger is not defined for SomeWordN as no bitwidth is known"
 
+instance (KnownNat n, 1 <= n) => QC.Arbitrary (WordN n) where
+  arbitrary = QC.arbitrarySizedBoundedIntegral
+  shrink = QC.shrinkIntegral
+
 minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n
 minusOneIntN _ = IntN (1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n)) - 1)
 
@@ -593,6 +620,10 @@
       n = fromIntegral (natVal (Proxy :: Proxy n))
       as = testBit a (n - 1)
       bs = testBit b (n - 1)
+
+instance (KnownNat n, 1 <= n) => QC.Arbitrary (IntN n) where
+  arbitrary = QC.arbitrarySizedBoundedIntegral
+  shrink = QC.shrinkIntegral
 
 instance SizedBV WordN where
   sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)
diff --git a/src/Grisette/Core/Data/Class/Bool.hs b/src/Grisette/Core/Data/Class/Bool.hs
--- a/src/Grisette/Core/Data/Class/Bool.hs
+++ b/src/Grisette/Core/Data/Class/Bool.hs
@@ -41,6 +41,7 @@
 import qualified Data.ByteString as B
 import Data.Functor.Sum
 import Data.Int
+import qualified Data.Text as T
 import Data.Word
 import GHC.TypeNats
 import Generics.Deriving
@@ -244,6 +245,7 @@
 CONCRETE_SEQ(Word32)
 CONCRETE_SEQ(Word64)
 CONCRETE_SEQ(B.ByteString)
+CONCRETE_SEQ(T.Text)
 CONCRETE_SEQ_BV(WordN)
 CONCRETE_SEQ_BV(IntN)
 CONCRETE_SEQ(SomeWordN)
diff --git a/src/Grisette/Core/Data/Class/Evaluate.hs b/src/Grisette/Core/Data/Class/Evaluate.hs
--- a/src/Grisette/Core/Data/Class/Evaluate.hs
+++ b/src/Grisette/Core/Data/Class/Evaluate.hs
@@ -34,6 +34,7 @@
 import Data.Functor.Sum
 import Data.Int
 import Data.Maybe
+import qualified Data.Text as T
 import Data.Word
 import GHC.TypeNats
 import Generics.Deriving
@@ -127,6 +128,7 @@
 CONCRETE_EVALUATESYM(SomeIntN)
 CONCRETE_EVALUATESYM(SomeWordN)
 CONCRETE_EVALUATESYM(B.ByteString)
+CONCRETE_EVALUATESYM(T.Text)
 CONCRETE_EVALUATESYM_BV(IntN)
 CONCRETE_EVALUATESYM_BV(WordN)
 #endif
diff --git a/src/Grisette/Core/Data/Class/ExtractSymbolics.hs b/src/Grisette/Core/Data/Class/ExtractSymbolics.hs
--- a/src/Grisette/Core/Data/Class/ExtractSymbolics.hs
+++ b/src/Grisette/Core/Data/Class/ExtractSymbolics.hs
@@ -32,6 +32,7 @@
 import qualified Data.ByteString as B
 import Data.Functor.Sum
 import Data.Int
+import qualified Data.Text as T
 import Data.Word
 import GHC.TypeNats
 import Generics.Deriving
@@ -115,6 +116,7 @@
 CONCRETE_EXTRACT_SYMBOLICS(SomeWordN)
 CONCRETE_EXTRACT_SYMBOLICS(SomeIntN)
 CONCRETE_EXTRACT_SYMBOLICS(B.ByteString)
+CONCRETE_EXTRACT_SYMBOLICS(T.Text)
 CONCRETE_EXTRACT_SYMBOLICS_BV(WordN)
 CONCRETE_EXTRACT_SYMBOLICS_BV(IntN)
 #endif
@@ -155,6 +157,71 @@
   instance
     (ExtractSymbolics a, ExtractSymbolics b, ExtractSymbolics c) =>
     ExtractSymbolics (a, b, c)
+
+-- (,,,)
+deriving via
+  (Default (a, b, c, d))
+  instance
+    ( ExtractSymbolics a,
+      ExtractSymbolics b,
+      ExtractSymbolics c,
+      ExtractSymbolics d
+    ) =>
+    ExtractSymbolics (a, b, c, d)
+
+-- (,,,,)
+deriving via
+  (Default (a, b, c, d, e))
+  instance
+    ( ExtractSymbolics a,
+      ExtractSymbolics b,
+      ExtractSymbolics c,
+      ExtractSymbolics d,
+      ExtractSymbolics e
+    ) =>
+    ExtractSymbolics (a, b, c, d, e)
+
+-- (,,,,,)
+deriving via
+  (Default (a, b, c, d, e, f))
+  instance
+    ( ExtractSymbolics a,
+      ExtractSymbolics b,
+      ExtractSymbolics c,
+      ExtractSymbolics d,
+      ExtractSymbolics e,
+      ExtractSymbolics f
+    ) =>
+    ExtractSymbolics (a, b, c, d, e, f)
+
+-- (,,,,,,)
+deriving via
+  (Default (a, b, c, d, e, f, g))
+  instance
+    ( ExtractSymbolics a,
+      ExtractSymbolics b,
+      ExtractSymbolics c,
+      ExtractSymbolics d,
+      ExtractSymbolics e,
+      ExtractSymbolics f,
+      ExtractSymbolics g
+    ) =>
+    ExtractSymbolics (a, b, c, d, e, f, g)
+
+-- (,,,,,,,)
+deriving via
+  (Default (a, b, c, d, e, f, g, h))
+  instance
+    ( ExtractSymbolics a,
+      ExtractSymbolics b,
+      ExtractSymbolics c,
+      ExtractSymbolics d,
+      ExtractSymbolics e,
+      ExtractSymbolics f,
+      ExtractSymbolics g,
+      ExtractSymbolics h
+    ) =>
+    ExtractSymbolics (a, b, c, d, e, f, g, h)
 
 -- MaybeT
 instance (ExtractSymbolics (m (Maybe a))) => ExtractSymbolics (MaybeT m a) where
diff --git a/src/Grisette/Core/Data/Class/GPretty.hs b/src/Grisette/Core/Data/Class/GPretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Grisette/Core/Data/Class/GPretty.hs
@@ -0,0 +1,376 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Grisette.Core.Data.Class.GPretty
+  ( GPretty (..),
+    groupedEnclose,
+    condEnclose,
+  )
+where
+
+import Control.Monad.Except
+import Control.Monad.Identity
+import Control.Monad.Trans.Maybe
+import qualified Control.Monad.Writer.Lazy as WriterLazy
+import qualified Control.Monad.Writer.Strict as WriterStrict
+import qualified Data.ByteString as B
+import Data.Functor.Sum
+import Data.Int
+import Data.Proxy
+import Data.String
+import qualified Data.Text as T
+import Data.Word
+import GHC.Generics
+import GHC.TypeLits
+import Generics.Deriving hiding (isNullary)
+import Grisette.Core.Data.BV
+
+#if MIN_VERSION_prettyprinter(1,7,0)
+import Prettyprinter
+#else
+import Data.Text.Prettyprint.Doc
+#endif
+
+glist :: [Doc ann] -> Doc ann
+glist l
+  | null l = "[]"
+  | length l == 1 = "[" <> head l <> "]"
+  | otherwise = groupedEnclose "[" "]" $ encloseSep "" "" (flatAlt ", " ",") l
+
+class GPretty a where
+  gpretty :: a -> Doc ann
+  gprettyPrec :: Int -> a -> Doc ann
+  gprettyList :: [a] -> Doc ann
+  gprettyList = align . glist . map gpretty
+
+  gpretty = gprettyPrec 0
+  gprettyPrec _ = gpretty
+
+  {-# MINIMAL gpretty | gprettyPrec #-}
+
+instance (Generic a, GPretty' (Rep a)) => GPretty (Default a) where
+  gprettyPrec i v = gprettyPrec' Pref i $ from $ unDefault v
+
+data Type = Rec | Tup | Pref | Inf String Int
+
+class GPretty' a where
+  gprettyPrec' :: Type -> Int -> a c -> Doc ann
+  isNullary :: a c -> Bool
+  isNullary = error "generic gpretty (isNullary): unnecessary case"
+
+instance GPretty' V1 where
+  gprettyPrec' _ _ x = case x of {}
+
+instance GPretty' U1 where
+  gprettyPrec' _ _ U1 = ""
+  isNullary _ = True
+
+instance (GPretty c) => GPretty' (K1 i c) where
+  gprettyPrec' _ n (K1 a) = gprettyPrec n a
+  isNullary _ = False
+
+groupedEnclose :: Doc ann -> Doc ann -> Doc ann -> Doc ann
+groupedEnclose l r d = group $ align $ vcat [l <> flatAlt " " "" <> d, r]
+
+condEnclose :: Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann
+condEnclose b = if b then groupedEnclose else const $ const id
+
+instance (GPretty' a, Constructor c) => GPretty' (M1 C c a) where
+  gprettyPrec' _ n c@(M1 x) =
+    case t of
+      Tup ->
+        prettyBraces t (gprettyPrec' t 0 x)
+      Inf _ m ->
+        group $ condEnclose (n > m) "(" ")" $ gprettyPrec' t m x
+      _ ->
+        if isNullary x
+          then pretty (conName c)
+          else
+            group $
+              condEnclose (n > 10) "(" ")" $
+                align $
+                  nest 2 $
+                    vsep
+                      [ pretty (conName c),
+                        prettyBraces t (gprettyPrec' t 11 x)
+                      ]
+    where
+      prettyBraces :: Type -> Doc ann -> Doc ann
+      prettyBraces Rec = groupedEnclose "{" "}"
+      prettyBraces Tup = groupedEnclose "(" ")"
+      prettyBraces Pref = id
+      prettyBraces (Inf _ _) = id
+      fixity = conFixity c
+      t
+        | conIsRecord c = Rec
+        | conIsTuple c = Tup
+        | otherwise = case fixity of
+            Prefix -> Pref
+            Infix _ i -> Inf (conName c) i
+      conIsTuple :: C1 c f p -> Bool
+      conIsTuple y = tupleName (conName y)
+        where
+          tupleName ('(' : ',' : _) = True
+          tupleName _ = False
+
+instance (Selector s, GPretty' a) => GPretty' (M1 S s a) where
+  gprettyPrec' t n s@(M1 x)
+    | selName s == "" =
+        case t of
+          Pref -> gprettyPrec' t (n + 1) x
+          _ -> gprettyPrec' t (n + 1) x
+    | otherwise =
+        pretty (selName s) <+> "=" <+> gprettyPrec' t 0 x
+  isNullary (M1 x) = isNullary x
+
+instance (GPretty' a) => GPretty' (M1 D d a) where
+  gprettyPrec' t n (M1 x) = gprettyPrec' t n x
+
+instance (GPretty' a, GPretty' b) => GPretty' (a :+: b) where
+  gprettyPrec' t n (L1 x) = gprettyPrec' t n x
+  gprettyPrec' t n (R1 x) = gprettyPrec' t n x
+
+instance (GPretty' a, GPretty' b) => GPretty' (a :*: b) where
+  gprettyPrec' t@Rec n (a :*: b) =
+    vcat
+      [ gprettyPrec' t n a,
+        "," <+> gprettyPrec' t n b
+      ]
+  gprettyPrec' t@(Inf s _) n (a :*: b) =
+    align $
+      nest 2 $
+        vsep
+          [ gprettyPrec' t n a,
+            pretty s <+> gprettyPrec' t n b
+          ]
+  gprettyPrec' t@Tup n (a :*: b) =
+    vcat
+      [ gprettyPrec' t 0 a,
+        "," <> flatAlt " " "" <> gprettyPrec' t 0 b
+      ]
+  gprettyPrec' t@Pref n (a :*: b) =
+    vsep
+      [ gprettyPrec' t (n + 1) a,
+        gprettyPrec' t (n + 1) b
+      ]
+  isNullary _ = False
+
+viaShowsPrec :: (Int -> a -> ShowS) -> Int -> a -> Doc ann
+viaShowsPrec f n a = pretty (f n a "")
+
+#define GPRETTY_SIMPLE(type) \
+instance GPretty type where gprettyPrec = viaShowsPrec showsPrec
+
+instance GPretty Char where
+  gpretty = viaShow
+  gprettyList v = pretty (fromString v :: T.Text)
+
+#if 1
+GPRETTY_SIMPLE(Bool)
+GPRETTY_SIMPLE(Integer)
+GPRETTY_SIMPLE(Int)
+GPRETTY_SIMPLE(Int8)
+GPRETTY_SIMPLE(Int16)
+GPRETTY_SIMPLE(Int32)
+GPRETTY_SIMPLE(Int64)
+GPRETTY_SIMPLE(Word)
+GPRETTY_SIMPLE(Word8)
+GPRETTY_SIMPLE(Word16)
+GPRETTY_SIMPLE(Word32)
+GPRETTY_SIMPLE(Word64)
+GPRETTY_SIMPLE(SomeIntN)
+GPRETTY_SIMPLE(SomeWordN)
+GPRETTY_SIMPLE(B.ByteString)
+GPRETTY_SIMPLE(T.Text)
+#endif
+
+instance (KnownNat n, 1 <= n) => GPretty (IntN n) where
+  gpretty = viaShow
+
+instance (KnownNat n, 1 <= n) => GPretty (WordN n) where
+  gpretty = viaShow
+
+-- ()
+instance GPretty () where
+  gpretty = viaShow
+
+-- Either
+deriving via
+  (Default (Either a b))
+  instance
+    (GPretty a, GPretty b) => GPretty (Either a b)
+
+-- Maybe
+deriving via
+  (Default (Maybe a))
+  instance
+    (GPretty a) => GPretty (Maybe a)
+
+-- List
+instance (GPretty a) => GPretty [a] where
+  gpretty = gprettyList
+
+-- (,)
+deriving via
+  (Default (a, b))
+  instance
+    (GPretty a, GPretty b) => GPretty (a, b)
+
+-- (,,)
+deriving via
+  (Default (a, b, c))
+  instance
+    (GPretty a, GPretty b, GPretty c) => GPretty (a, b, c)
+
+-- (,,,)
+deriving via
+  (Default (a, b, c, d))
+  instance
+    ( GPretty a,
+      GPretty b,
+      GPretty c,
+      GPretty d
+    ) =>
+    GPretty (a, b, c, d)
+
+-- (,,,,)
+deriving via
+  (Default (a, b, c, d, e))
+  instance
+    ( GPretty a,
+      GPretty b,
+      GPretty c,
+      GPretty d,
+      GPretty e
+    ) =>
+    GPretty (a, b, c, d, e)
+
+-- (,,,,,)
+deriving via
+  (Default (a, b, c, d, e, f))
+  instance
+    ( GPretty a,
+      GPretty b,
+      GPretty c,
+      GPretty d,
+      GPretty e,
+      GPretty f
+    ) =>
+    GPretty (a, b, c, d, e, f)
+
+-- (,,,,,,)
+deriving via
+  (Default (a, b, c, d, e, f, g))
+  instance
+    ( GPretty a,
+      GPretty b,
+      GPretty c,
+      GPretty d,
+      GPretty e,
+      GPretty f,
+      GPretty g
+    ) =>
+    GPretty (a, b, c, d, e, f, g)
+
+-- (,,,,,,,)
+deriving via
+  (Default (a, b, c, d, e, f, g, h))
+  instance
+    ( GPretty a,
+      GPretty b,
+      GPretty c,
+      GPretty d,
+      GPretty e,
+      GPretty f,
+      GPretty g,
+      GPretty h
+    ) =>
+    GPretty (a, b, c, d, e, f, g, h)
+
+-- Sum
+deriving via
+  (Default (Sum f g a))
+  instance
+    (GPretty (f a), GPretty (g a)) =>
+    GPretty (Sum f g a)
+
+-- MaybeT
+instance
+  (GPretty (m (Maybe a))) =>
+  GPretty (MaybeT m a)
+  where
+  gprettyPrec i (MaybeT a) =
+    group $
+      nest 2 $
+        vsep
+          [ "MaybeT",
+            gprettyPrec 11 a
+          ]
+
+-- ExceptT
+instance
+  (GPretty (m (Either e a))) =>
+  GPretty (ExceptT e m a)
+  where
+  gprettyPrec i (ExceptT a) =
+    group $
+      nest 2 $
+        vsep
+          [ "ExceptT",
+            gprettyPrec 11 a
+          ]
+
+-- WriterT
+instance
+  (GPretty (m (a, w))) =>
+  GPretty (WriterLazy.WriterT w m a)
+  where
+  gprettyPrec i (WriterLazy.WriterT a) =
+    group $
+      nest 2 $
+        vsep
+          [ "WriterT",
+            gprettyPrec 11 a
+          ]
+
+instance
+  (GPretty (m (a, w))) =>
+  GPretty (WriterStrict.WriterT w m a)
+  where
+  gprettyPrec i (WriterStrict.WriterT a) =
+    group $
+      nest 2 $
+        vsep
+          [ "WriterT",
+            gprettyPrec 11 a
+          ]
+
+-- Identity
+instance (GPretty a) => GPretty (Identity a) where
+  gprettyPrec i (Identity a) =
+    group $
+      nest 2 $
+        vsep
+          [ "Identity",
+            gprettyPrec 11 a
+          ]
+
+-- IdentityT
+instance (GPretty (m a)) => GPretty (IdentityT m a) where
+  gprettyPrec i (IdentityT a) =
+    group $
+      nest 2 $
+        vsep
+          [ "IdentityT",
+            gprettyPrec 11 a
+          ]
diff --git a/src/Grisette/Core/Data/Class/GenSym.hs b/src/Grisette/Core/Data/Class/GenSym.hs
--- a/src/Grisette/Core/Data/Class/GenSym.hs
+++ b/src/Grisette/Core/Data/Class/GenSym.hs
@@ -87,6 +87,7 @@
 import Data.Hashable
 import Data.Int
 import Data.String
+import qualified Data.Text as T
 import Data.Typeable
 import Data.Word
 import GHC.TypeNats
@@ -760,6 +761,7 @@
 CONCRETE_GENSYM_SAME_SHAPE(SomeWordN)
 CONCRETE_GENSYM_SAME_SHAPE(SomeIntN)
 CONCRETE_GENSYM_SAME_SHAPE(B.ByteString)
+CONCRETE_GENSYM_SAME_SHAPE(T.Text)
 CONCRETE_GENSYM_SAME_SHAPE_BV(WordN)
 CONCRETE_GENSYM_SAME_SHAPE_BV(IntN)
 
@@ -779,6 +781,7 @@
 CONCRETE_GENSYMSIMPLE_SAME_SHAPE(SomeWordN)
 CONCRETE_GENSYMSIMPLE_SAME_SHAPE(SomeIntN)
 CONCRETE_GENSYMSIMPLE_SAME_SHAPE(B.ByteString)
+CONCRETE_GENSYMSIMPLE_SAME_SHAPE(T.Text)
 CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(WordN)
 CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(IntN)
 #endif
diff --git a/src/Grisette/Core/Data/Class/Mergeable.hs b/src/Grisette/Core/Data/Class/Mergeable.hs
--- a/src/Grisette/Core/Data/Class/Mergeable.hs
+++ b/src/Grisette/Core/Data/Class/Mergeable.hs
@@ -68,6 +68,7 @@
 import Data.Int
 import Data.Kind
 import qualified Data.Monoid as Monoid
+import qualified Data.Text as T
 import Data.Typeable
 import Data.Word
 import GHC.Natural
@@ -458,6 +459,7 @@
 CONCRETE_ORD_MERGEABLE(Word32)
 CONCRETE_ORD_MERGEABLE(Word64)
 CONCRETE_ORD_MERGEABLE(B.ByteString)
+CONCRETE_ORD_MERGEABLE(T.Text)
 CONCRETE_ORD_MERGEABLE_BV(WordN)
 CONCRETE_ORD_MERGEABLE_BV(IntN)
 #endif
diff --git a/src/Grisette/Core/Data/Class/SOrd.hs b/src/Grisette/Core/Data/Class/SOrd.hs
--- a/src/Grisette/Core/Data/Class/SOrd.hs
+++ b/src/Grisette/Core/Data/Class/SOrd.hs
@@ -34,6 +34,7 @@
 import qualified Data.ByteString as B
 import Data.Functor.Sum
 import Data.Int
+import qualified Data.Text as T
 import Data.Word
 import GHC.TypeLits
 import Generics.Deriving
@@ -249,6 +250,7 @@
 CONCRETE_SORD(SomeWordN)
 CONCRETE_SORD(SomeIntN)
 CONCRETE_SORD(B.ByteString)
+CONCRETE_SORD(T.Text)
 CONCRETE_SORD_BV(WordN)
 CONCRETE_SORD_BV(IntN)
 #endif
diff --git a/src/Grisette/Core/Data/Class/Substitute.hs b/src/Grisette/Core/Data/Class/Substitute.hs
--- a/src/Grisette/Core/Data/Class/Substitute.hs
+++ b/src/Grisette/Core/Data/Class/Substitute.hs
@@ -33,6 +33,7 @@
 import qualified Data.ByteString as B
 import Data.Functor.Sum
 import Data.Int
+import qualified Data.Text as T
 import Data.Word
 import GHC.TypeNats
 import Generics.Deriving
@@ -119,6 +120,7 @@
 CONCRETE_SUBSTITUTESYM(SomeWordN)
 CONCRETE_SUBSTITUTESYM(SomeIntN)
 CONCRETE_SUBSTITUTESYM(B.ByteString)
+CONCRETE_SUBSTITUTESYM(T.Text)
 CONCRETE_SUBSTITUTESYM_BV(WordN)
 CONCRETE_SUBSTITUTESYM_BV(IntN)
 #endif
diff --git a/src/Grisette/Core/Data/Class/ToCon.hs b/src/Grisette/Core/Data/Class/ToCon.hs
--- a/src/Grisette/Core/Data/Class/ToCon.hs
+++ b/src/Grisette/Core/Data/Class/ToCon.hs
@@ -32,6 +32,7 @@
 import qualified Data.ByteString as B
 import Data.Functor.Sum
 import Data.Int
+import qualified Data.Text as T
 import Data.Word
 import GHC.Generics
 import GHC.TypeNats
@@ -113,6 +114,7 @@
 CONCRETE_TOCON(SomeWordN)
 CONCRETE_TOCON(SomeIntN)
 CONCRETE_TOCON(B.ByteString)
+CONCRETE_TOCON(T.Text)
 CONCRETE_TOCON_BV(WordN)
 CONCRETE_TOCON_BV(IntN)
 #endif
diff --git a/src/Grisette/Core/Data/Class/ToSym.hs b/src/Grisette/Core/Data/Class/ToSym.hs
--- a/src/Grisette/Core/Data/Class/ToSym.hs
+++ b/src/Grisette/Core/Data/Class/ToSym.hs
@@ -35,6 +35,7 @@
 import qualified Data.ByteString as B
 import Data.Functor.Sum
 import Data.Int
+import qualified Data.Text as T
 import Data.Word
 import GHC.TypeNats
 import Generics.Deriving
@@ -101,6 +102,7 @@
 CONCRETE_TOSYM(SomeIntN)
 CONCRETE_TOSYM(SomeWordN)
 CONCRETE_TOSYM(B.ByteString)
+CONCRETE_TOSYM(T.Text)
 CONCRETE_TOSYM_BV(IntN)
 CONCRETE_TOSYM_BV(WordN)
 #endif
diff --git a/src/Grisette/Core/Data/Union.hs b/src/Grisette/Core/Data/Union.hs
--- a/src/Grisette/Core/Data/Union.hs
+++ b/src/Grisette/Core/Data/Union.hs
@@ -1,7 +1,9 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeFamilies #-}
 
@@ -29,12 +31,19 @@
 import Data.Hashable
 import GHC.Generics
 import Grisette.Core.Data.Class.Bool
+import Grisette.Core.Data.Class.GPretty
 import Grisette.Core.Data.Class.Mergeable
 import Grisette.Core.Data.Class.SimpleMergeable
 import Grisette.Core.Data.Class.Solvable
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim
 import Language.Haskell.TH.Syntax
 
+#if MIN_VERSION_prettyprinter(1,7,0)
+import Prettyprinter
+#else
+import Data.Text.Prettyprint.Doc
+#endif
+
 -- | The default union implementation.
 data Union a
   = -- | A single value
@@ -123,6 +132,20 @@
 
 instance (Show a) => Show (Union a) where
   showsPrec = showsPrec1
+
+instance (GPretty a) => GPretty (Union a) where
+  gprettyPrec n (Single a) = gprettyPrec n a
+  gprettyPrec n (If _ _ cond t f) =
+    group $
+      condEnclose (n > 10) "(" ")" $
+        align $
+          nest 2 $
+            vsep
+              [ "If",
+                gprettyPrec 11 cond,
+                gprettyPrec 11 t,
+                gprettyPrec 11 f
+              ]
 
 instance (Hashable a) => Hashable (Union a) where
   s `hashWithSalt` (Single a) = s `hashWithSalt` (0 :: Int) `hashWithSalt` a
diff --git a/src/Grisette/Experimental/GenSymConstrained.hs b/src/Grisette/Experimental/GenSymConstrained.hs
--- a/src/Grisette/Experimental/GenSymConstrained.hs
+++ b/src/Grisette/Experimental/GenSymConstrained.hs
@@ -30,7 +30,6 @@
 
 import Control.Monad.Except
 import Control.Monad.Trans.Maybe
-import qualified Data.ByteString as B
 import Data.Int
 import Data.Word
 import Debug.Trace
diff --git a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
--- a/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
+++ b/src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
@@ -9,6 +10,8 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
@@ -44,6 +47,7 @@
     UTerm (..),
     type (-->) (..),
     buildGeneralFun,
+    prettyPrintTerm,
   )
 where
 
@@ -71,6 +75,12 @@
 import Language.Haskell.TH.Syntax.Compat
 import Type.Reflection
 
+#if MIN_VERSION_prettyprinter(1,7,0)
+import Prettyprinter
+#else
+import Data.Text.Prettyprint.Doc
+#endif
+
 -- $setup
 -- >>> import Grisette.Core
 -- >>> import Grisette.IR.SymPrim
@@ -556,6 +566,21 @@
     "QuotBoundedIntegral{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"
   show (RemBoundedIntegralTerm i arg1 arg2) =
     "RemBoundedIntegral{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"
+
+prettyPrintTerm :: Term t -> Doc ann
+prettyPrintTerm v =
+  column
+    ( \c ->
+        pageWidth $ \case
+          AvailablePerLine i r ->
+            if fromIntegral (c + len) > fromIntegral i * r
+              then "..."
+              else pretty formatted
+          Unbounded -> pretty formatted
+    )
+  where
+    formatted = introSupportedPrimConstraint v $ pformat v
+    len = length formatted
 
 instance (SupportedPrim t) => Eq (Term t) where
   (==) = (==) `on` identity
diff --git a/src/Grisette/IR/SymPrim/Data/SymPrim.hs b/src/Grisette/IR/SymPrim/Data/SymPrim.hs
--- a/src/Grisette/IR/SymPrim/Data/SymPrim.hs
+++ b/src/Grisette/IR/SymPrim/Data/SymPrim.hs
@@ -69,6 +69,7 @@
 import Data.Int
 import Data.Proxy
 import Data.String
+import qualified Data.Text as T
 import Data.Typeable
 import Data.Word
 import GHC.Generics
@@ -82,6 +83,7 @@
 import Grisette.Core.Data.Class.Evaluate
 import Grisette.Core.Data.Class.ExtractSymbolics
 import Grisette.Core.Data.Class.Function
+import Grisette.Core.Data.Class.GPretty
 import Grisette.Core.Data.Class.GenSym
 import Grisette.Core.Data.Class.Mergeable
 import Grisette.Core.Data.Class.ModelOps
@@ -606,6 +608,34 @@
 
 -- Aggregate instances
 
+-- Prettyprint
+#define GPRETTY_SYM_SIMPLE(symtype) \
+instance GPretty symtype where \
+  gpretty (symtype t) = prettyPrintTerm t
+
+#define GPRETTY_SYM_BV(symtype) \
+instance (KnownNat n, 1 <= n) => GPretty (symtype n) where \
+  gpretty (symtype t) = prettyPrintTerm t
+
+#define GPRETTY_SYM_FUN(op, cons) \
+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb)\
+  => GPretty (sa op sb) where \
+  gpretty (cons t) = prettyPrintTerm t
+
+#define GPRETTY_SYM_SOME_BV(symtype) \
+instance GPretty symtype where \
+  gpretty (symtype t) = gpretty t
+
+#if 1
+GPRETTY_SYM_SIMPLE(SymBool)
+GPRETTY_SYM_SIMPLE(SymInteger)
+GPRETTY_SYM_BV(SymIntN)
+GPRETTY_SYM_BV(SymWordN)
+GPRETTY_SYM_FUN(=~>, SymTabularFun)
+GPRETTY_SYM_FUN(-~>, SymGeneralFun)
+GPRETTY_SYM_SOME_BV(SomeSymIntN)
+GPRETTY_SYM_SOME_BV(SomeSymWordN)
+#endif
 -- Num
 
 #define NUM_BV(symtype) \
@@ -1509,6 +1539,7 @@
 CONCRETE_ALLSYMS(Word32)
 CONCRETE_ALLSYMS(Word64)
 CONCRETE_ALLSYMS(B.ByteString)
+CONCRETE_ALLSYMS(T.Text)
 ALLSYMS_SIMPLE(SymBool)
 ALLSYMS_SIMPLE(SymInteger)
 ALLSYMS_BV(SymIntN)
diff --git a/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot b/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
--- a/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
+++ b/src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot
@@ -38,6 +38,7 @@
 import Grisette.Core.Data.BV
 import Grisette.Core.Data.Class.Evaluate
 import Grisette.Core.Data.Class.ExtractSymbolics
+import Grisette.Core.Data.Class.GPretty
 import Grisette.Core.Data.Class.Solvable
 import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
 import Grisette.IR.SymPrim.Data.TabularFun
@@ -89,6 +90,8 @@
 instance EvaluateSym SymBool
 
 instance ExtractSymbolics SymBool
+
+instance GPretty SymBool
 
 newtype SymInteger = SymInteger {underlyingIntegerTerm :: Term Integer}
 
diff --git a/test/Grisette/Core/Data/BVTests.hs b/test/Grisette/Core/Data/BVTests.hs
--- a/test/Grisette/Core/Data/BVTests.hs
+++ b/test/Grisette/Core/Data/BVTests.hs
@@ -420,6 +420,13 @@
             sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b1010000 :: IntN 8) @=? 0b10
         ],
       testGroup
+        "read"
+        [ testProperty "read . show" $ \(x :: IntN 8) -> read (show x) == x,
+          testProperty "read . show" $ \(x :: WordN 8) -> read (show x) == x,
+          testProperty "read . show" $ \(x :: IntN 9) -> read (show x) == x,
+          testProperty "read . show" $ \(x :: WordN 9) -> read (show x) == x
+        ],
+      testGroup
         "Regression"
         [ testCase "division of min bound and minus one for signed bit vector should throw" $ do
             shouldThrow "divMod" $ divMod (minBound :: IntN 8) (-1 :: IntN 8)
diff --git a/test/Grisette/Core/Data/Class/GPrettyTests.hs b/test/Grisette/Core/Data/Class/GPrettyTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Grisette/Core/Data/Class/GPrettyTests.hs
@@ -0,0 +1,342 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Grisette.Core.Data.Class.GPrettyTests where
+
+import Data.Int
+import Data.Text as T
+import Data.Word
+import GHC.Generics
+import GHC.Stack
+import Generics.Deriving
+import Grisette.Core.Data.BV
+import Grisette.Core.Data.Class.Bool
+import Grisette.Core.Data.Class.GPretty
+import Grisette.IR.SymPrim.Data.SymPrim
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck hiding ((.&.))
+
+#if MIN_VERSION_prettyprinter(1,7,0)
+import Prettyprinter
+import Prettyprinter.Render.Text
+#else
+import Data.Text.Prettyprint.Doc
+import Data.Text.Prettyprint.Doc.Render.Text
+#endif
+
+testGPretty :: (HasCallStack, GPretty a) => String -> Int -> a -> T.Text -> TestTree
+testGPretty n i a s =
+  testCase n $
+    renderStrict
+      ( layoutPretty
+          (LayoutOptions $ AvailablePerLine i 1)
+          (gpretty a)
+      )
+      @=? s
+
+propertyGPrettyShow ::
+  forall proxy a.
+  (HasCallStack, GPretty a, Show a) =>
+  String ->
+  Gen a ->
+  TestTree
+propertyGPrettyShow n g =
+  testProperty n $ forAll g $ \(a :: a) -> do
+    renderStrict (layoutPretty (LayoutOptions Unbounded) (gpretty a)) == T.pack (show a)
+
+propertyGPrettyRead ::
+  forall proxy a.
+  (HasCallStack, GPretty a, Read a, Show a, Eq a) =>
+  String ->
+  Gen a ->
+  TestTree
+propertyGPrettyRead n g =
+  testProperty n $ \i -> forAll g $ \(a :: a) -> do
+    read
+      ( T.unpack
+          ( renderStrict
+              ( layoutPretty
+                  (LayoutOptions $ AvailablePerLine (abs i) 0.8)
+                  (gpretty a)
+              )
+          )
+      )
+      == a
+
+propertyGPretty ::
+  forall proxy a.
+  (HasCallStack, GPretty a, Read a, Show a, Eq a) =>
+  String ->
+  Gen a ->
+  TestTree
+propertyGPretty n g =
+  testGroup
+    n
+    [ propertyGPrettyShow "single line" g,
+      propertyGPrettyRead "compact" g
+    ]
+
+data I5 a b = a :-: b
+  deriving (Generic, Show, Read, Eq)
+  deriving (GPretty) via (Default (I5 a b))
+
+infixl 5 :-:
+
+data I6 a b = a :--: b
+  deriving (Generic, Show, Read, Eq)
+  deriving (GPretty) via (Default (I6 a b))
+
+infixl 6 :--:
+
+instance
+  (Arbitrary a, Arbitrary b) =>
+  Arbitrary (I5 a b)
+  where
+  arbitrary = do
+    a <- arbitrary
+    b <- arbitrary
+    return $ a :-: b
+
+instance
+  (Arbitrary a, Arbitrary b) =>
+  Arbitrary (I6 a b)
+  where
+  arbitrary = do
+    a <- arbitrary
+    b <- arbitrary
+    return $ a :--: b
+
+data Record a b = Record {ra :: a, rb :: b}
+  deriving (Generic, Show, Read, Eq)
+  deriving (GPretty) via (Default (Record a b))
+
+instance
+  (Arbitrary a, Arbitrary b) =>
+  Arbitrary (Record a b)
+  where
+  arbitrary = do
+    a <- arbitrary
+    Record a <$> arbitrary
+
+gprettyTests :: TestTree
+gprettyTests =
+  testGroup
+    "GPrettyTests"
+    [ testGroup
+        "simple tests"
+        [ propertyGPretty "Bool" (arbitrary :: Gen Bool),
+          propertyGPretty "Integer" (arbitrary :: Gen Integer),
+          propertyGPretty "Int" (arbitrary :: Gen Int),
+          propertyGPretty "Int8" (arbitrary :: Gen Int8),
+          propertyGPretty "Int16" (arbitrary :: Gen Int16),
+          propertyGPretty "Int32" (arbitrary :: Gen Int32),
+          propertyGPretty "Int64" (arbitrary :: Gen Int64),
+          propertyGPretty "Word" (arbitrary :: Gen Word),
+          propertyGPretty "Word8" (arbitrary :: Gen Word8),
+          propertyGPretty "Word16" (arbitrary :: Gen Word16),
+          propertyGPretty "Word32" (arbitrary :: Gen Word32),
+          propertyGPretty "Word64" (arbitrary :: Gen Word64),
+          propertyGPrettyShow
+            "SomeWordN"
+            ( oneof
+                [ SomeWordN <$> (arbitrary :: Gen (WordN 8)),
+                  SomeWordN <$> (arbitrary :: Gen (WordN 9)),
+                  SomeWordN <$> (arbitrary :: Gen (WordN 10))
+                ]
+            ),
+          propertyGPretty "WordN 8" (arbitrary :: Gen (WordN 8)),
+          propertyGPretty "WordN 9" (arbitrary :: Gen (WordN 9)),
+          propertyGPrettyShow
+            "SomeIntN"
+            ( oneof
+                [ SomeIntN <$> (arbitrary :: Gen (IntN 8)),
+                  SomeIntN <$> (arbitrary :: Gen (IntN 9)),
+                  SomeIntN <$> (arbitrary :: Gen (IntN 10))
+                ]
+            ),
+          propertyGPretty "IntN 8" (arbitrary :: Gen (IntN 8)),
+          propertyGPretty "IntN 9" (arbitrary :: Gen (IntN 9)),
+          propertyGPretty "()" (arbitrary :: Gen ()),
+          propertyGPretty
+            "Either"
+            ( arbitrary :: Gen (Either Int Bool)
+            ),
+          propertyGPretty
+            "Maybe"
+            ( arbitrary :: Gen (Maybe Int)
+            ),
+          propertyGPretty
+            "List"
+            ( arbitrary :: Gen [Int]
+            ),
+          propertyGPretty
+            "(,)"
+            ( arbitrary :: Gen (Int, Int)
+            ),
+          propertyGPretty
+            "(,,)"
+            ( arbitrary :: Gen (Int, Int, Int)
+            ),
+          propertyGPretty
+            "(,,,)"
+            ( arbitrary :: Gen (Int, Int, Int, Int)
+            ),
+          propertyGPretty
+            "(,,,,)"
+            ( arbitrary :: Gen (Int, Int, Int, Int, Int)
+            ),
+          propertyGPretty
+            "(,,,,,)"
+            ( arbitrary :: Gen (Int, Int, Int, Int, Int, Int)
+            ),
+          propertyGPretty
+            "(,,,,,,)"
+            ( arbitrary :: Gen (Int, Int, Int, Int, Int, Int, Int)
+            ),
+          propertyGPretty
+            "(,,,,,,,)"
+            ( arbitrary :: Gen (Int, Int, Int, Int, Int, Int, Int, Int)
+            ),
+          propertyGPretty
+            "I5"
+            ( arbitrary :: Gen (I5 Int Int)
+            ),
+          propertyGPretty
+            "Record"
+            ( arbitrary :: Gen (Record Int Int)
+            )
+        ],
+      testGroup
+        "Combined types"
+        [ propertyGPretty
+            "Maybe Maybe"
+            ( arbitrary :: Gen (Maybe (Maybe Int))
+            ),
+          propertyGPretty
+            "Maybe (,)"
+            ( arbitrary :: Gen (Maybe (Int, Int))
+            ),
+          propertyGPretty
+            "Maybe I5"
+            ( arbitrary :: Gen (Maybe (I5 Int Int))
+            ),
+          propertyGPretty
+            "Maybe []"
+            ( arbitrary :: Gen (Maybe [Int])
+            ),
+          propertyGPretty
+            "Maybe Record"
+            ( arbitrary :: Gen (Maybe (Record Int Int))
+            ),
+          propertyGPretty
+            "(Maybe,Either)"
+            ( arbitrary :: Gen (Maybe Int, Either Int Int)
+            ),
+          propertyGPretty
+            "((,),(,))"
+            ( arbitrary :: Gen ((Int, Int), (Int, Int))
+            ),
+          propertyGPretty
+            "(I5,I5)"
+            ( arbitrary :: Gen (I5 Int Int, I5 Int Int)
+            ),
+          propertyGPretty
+            "([],[])"
+            ( arbitrary :: Gen ([Int], [Int])
+            ),
+          propertyGPretty
+            "(Record,Record)"
+            ( arbitrary :: Gen (Record Int Int, Record Int Int)
+            ),
+          propertyGPretty
+            "I5 Maybe Either"
+            ( arbitrary :: Gen (I5 (Maybe Int) (Either Int Int))
+            ),
+          propertyGPretty
+            "I5 (,) (,)"
+            ( arbitrary :: Gen (I5 (Int, Int) (Int, Int))
+            ),
+          propertyGPretty
+            "I5 I6 I6"
+            ( arbitrary :: Gen (I5 (I6 Int Int) (I6 Int Int))
+            ),
+          propertyGPretty
+            "I5 I5 I5"
+            ( arbitrary :: Gen (I5 (I5 Int Int) (I5 Int Int))
+            ),
+          propertyGPretty
+            "I6 I5 I5"
+            ( arbitrary :: Gen (I6 (I5 Int Int) (I5 Int Int))
+            ),
+          propertyGPretty
+            "I6 I6 I6"
+            ( arbitrary :: Gen (I6 (I6 Int Int) (I6 Int Int))
+            ),
+          propertyGPretty
+            "I5 [] []"
+            ( arbitrary :: Gen (I5 [Int] [Int])
+            ),
+          propertyGPretty
+            "I5 Record Record"
+            ( arbitrary :: Gen (I5 (Record Int Int) (Record Int Int))
+            ),
+          propertyGPretty
+            "[Maybe]"
+            ( arbitrary :: Gen [Maybe Int]
+            ),
+          propertyGPretty
+            "[(,)]"
+            ( arbitrary :: Gen [(Int, Int)]
+            ),
+          propertyGPretty
+            "[I5]"
+            ( arbitrary :: Gen [I5 Int Int]
+            ),
+          propertyGPretty
+            "[[]]"
+            ( arbitrary :: Gen [[Int]]
+            ),
+          propertyGPretty
+            "[Record]"
+            ( arbitrary :: Gen [Record Int Int]
+            ),
+          propertyGPretty
+            "Record Maybe Either"
+            ( arbitrary :: Gen (Record (Maybe Int) (Either Int Int))
+            ),
+          propertyGPretty
+            "Record (,) (,)"
+            ( arbitrary :: Gen (Record (Int, Int) (Int, Int))
+            ),
+          propertyGPretty
+            "Record I5 I6"
+            ( arbitrary :: Gen (Record (I5 Int Int) (I6 Int Int))
+            ),
+          propertyGPretty
+            "Record []"
+            ( arbitrary :: Gen (Record [Int] [Int])
+            ),
+          propertyGPretty
+            "Record Record"
+            ( arbitrary :: Gen (Record (Record Int Int) (Record Int Int))
+            )
+        ],
+      testGroup
+        "Symbolic types"
+        [ testGPretty
+            "enough space"
+            80
+            ("a" &&~ "b" :: SymBool)
+            "(&& a b)",
+          testGPretty
+            "not enough space"
+            6
+            ("a" &&~ "b" :: SymBool)
+            "..."
+        ]
+    ]
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -27,6 +27,7 @@
 import Grisette.Backend.SBV.Data.SMT.TermRewritingTests
 import Grisette.Core.Control.Monad.UnionMTests
 import qualified Grisette.Core.Data.BVTests
+import Grisette.Core.Data.Class.GPrettyTests
 import qualified Grisette.IR.SymPrim.Data.Prim.BVTests
 import Grisette.IR.SymPrim.Data.Prim.BitsTests
 import Grisette.IR.SymPrim.Data.Prim.BoolTests
@@ -56,9 +57,17 @@
 coreTests :: TestTree
 coreTests =
   testGroup
-    "Grisette.Core.Control.Monad.UnionM"
-    [ unionMTests,
-      Grisette.Core.Data.BVTests.bvTests
+    "core"
+    [ testGroup
+        "Grisette.Core.Control.Monad.UnionM"
+        [unionMTests],
+      testGroup
+        "Grisette.Core.Data"
+        [ testGroup
+            "Class"
+            [gprettyTests],
+          Grisette.Core.Data.BVTests.bvTests
+        ]
     ]
 
 {-