diff --git a/library/Refined.hs b/library/Refined.hs
--- a/library/Refined.hs
+++ b/library/Refined.hs
@@ -127,6 +127,9 @@
   , RefineM, refineM, runRefineM
   , throwRefine, catchRefine
   , throwRefineOtherException
+
+    -- * Re-Exports
+  , pretty
   ) where
 
 --------------------------------------------------------------------------------
diff --git a/library/Refined/Internal.hs b/library/Refined/Internal.hs
--- a/library/Refined/Internal.hs
+++ b/library/Refined/Internal.hs
@@ -32,13 +32,16 @@
 
 --------------------------------------------------------------------------------
 
+{-# LANGUAGE CPP                        #-}
 {-# LANGUAGE DataKinds                  #-}
 {-# LANGUAGE DeriveFoldable             #-}
 {-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE ExistentialQuantification  #-}
 {-# LANGUAGE ExplicitNamespaces         #-}
 {-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase                 #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
 {-# LANGUAGE OverloadedStrings          #-}
 {-# LANGUAGE QuasiQuotes                #-}
@@ -103,6 +106,7 @@
   , NonNegative
   , ZeroToOne
   , NonZero
+  , NegativeFromTo
 
     -- * Foldable predicates
   , SizeLessThan
@@ -140,26 +144,28 @@
  
   , (|>)
   , (.>)
+
+    -- * Re-Exports
+  , PP.pretty
  ) where
 
 --------------------------------------------------------------------------------
 
 import           Prelude
-                 (Num, fromIntegral, undefined)
+                 (Num, fromIntegral, negate, undefined)
 
 import           Control.Applicative          (Applicative (pure))
 import           Control.Exception            (Exception (displayException))
-import           Control.Monad                (Monad, unless, when)
+import           Control.Monad                (Monad, unless)
 import           Data.Bool                    (Bool(True,False),(&&), otherwise)
 import           Data.Coerce                  (coerce)
 import           Data.Either
-                 (Either (Left, Right), either, isRight)
+                 (Either (Left, Right), either)
 import           Data.Eq                      (Eq, (==), (/=))
 import           Data.Foldable                (Foldable(length, foldl'))
 import           Data.Function                (const, flip, ($), (.))
 import           Data.Functor                 (Functor, fmap)
 import           Data.Functor.Identity        (Identity (runIdentity))
-import           Data.List                    ((++))
 import           Data.Monoid                  (mconcat)
 import           Data.Ord                     (Ord, (<), (<=), (>), (>=))
 import           Data.Proxy                   (Proxy (Proxy))
@@ -183,7 +189,7 @@
 import           GHC.Generics                 (Generic, Generic1)
 import           GHC.TypeLits                 (type (<=), KnownNat, Nat, natVal)
 
-import           Refined.These                (These(This,That,These))
+import           Data.These                   (These(This,That,These))
 
 import qualified Data.Text.Prettyprint.Doc    as PP
 import qualified Language.Haskell.TH.Syntax   as TH
@@ -317,14 +323,15 @@
 --
 --   It may be useful to use this function with the `th-lift-instances` package at https://hackage.haskell.org/package/th-lift-instances/
 refineTH :: (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x))
-refineTH = let refineByResult :: (Predicate p x)
-                              => TH.Q (TH.TExp (Refined p x))
-                              -> x
-                              -> Either RefineException (Refined p x)
-               refineByResult = const refine
-           in fix $ \loop -> refineByResult (loop undefined)
-                             .> either (show .> fail) TH.lift
-                             .> fmap TH.TExp
+refineTH =
+  let refineByResult :: (Predicate p x)
+        => TH.Q (TH.TExp (Refined p x))
+        -> x
+        -> Either RefineException (Refined p x)
+      refineByResult = const refine
+  in fix $ \loop -> refineByResult (loop undefined)
+                    .> either (show .> fail) TH.lift
+                    .> fmap TH.TExp
 
 --------------------------------------------------------------------------------
 
@@ -351,6 +358,7 @@
 
 instance Predicate IdPred x where
   validate _ _ = pure ()
+  {-# INLINE validate #-}
 
 --------------------------------------------------------------------------------
 
@@ -361,8 +369,9 @@
 instance (Predicate p x, Typeable p) => Predicate (Not p) x where
   validate p x = do
     result <- runRefineT (validate @p undefined x)
-    when (isRight result) $ do
-      throwRefine (RefineNotException (typeOf p))
+    case result of
+      Left r -> throwRefine (RefineNotException (typeOf p) r)
+      Right () -> pure ()
 
 --------------------------------------------------------------------------------
 
@@ -418,8 +427,14 @@
         sz = length x
     unless (sz < fromIntegral x') $ do
       throwRefineOtherException (typeOf p)
-        $ "Size of Foldable is not less than " <> PP.pretty x' <> "\n"
-        <> "\tSize is: " <> PP.pretty sz
+        ( [ "Size of Foldable is not less than "
+          , PP.pretty x'
+          , newline
+          , twoSpaces
+          , "Size is: "
+          , PP.pretty sz
+          ] |> mconcat
+        )
 
 --------------------------------------------------------------------------------
 
@@ -434,8 +449,14 @@
         sz = length x
     unless (sz > fromIntegral x') $ do
       throwRefineOtherException (typeOf p)
-        $ "Size of Foldable is not greater than " <> PP.pretty x' <> "\n"
-        <> "\tSize is: " <> PP.pretty sz
+        ( [ "Size of Foldable is not greater than "
+          , PP.pretty x'
+          , newline
+          , twoSpaces
+          , "Size is: "
+          , PP.pretty sz
+          ] |> mconcat
+        )
 
 --------------------------------------------------------------------------------
 
@@ -450,8 +471,14 @@
         sz = length x
     unless (sz == fromIntegral x') $ do
       throwRefineOtherException (typeOf p)
-        $ "Size of Foldable is not equal to " <> PP.pretty x' <> "\n"
-        <> "\tSize is: " <> PP.pretty sz
+        ( [ "Size of Foldable is not equal to "
+          , PP.pretty x'
+          , newline
+          , twoSpaces
+          , "Size is: "
+          , PP.pretty sz
+          ] |> mconcat
+        )
 
 --------------------------------------------------------------------------------
 
@@ -463,8 +490,7 @@
 instance (Foldable t, Ord a) => Predicate Ascending (t a) where
   validate p x = do
     unless (increasing x) $ do
-      throwRefineOtherException (typeOf p)
-        $ "Foldable is not in ascending order "
+      throwRefineOtherException (typeOf p) ( "Foldable is not in ascending order." )
 
 --------------------------------------------------------------------------------
 
@@ -476,8 +502,7 @@
 instance (Foldable t, Ord a) => Predicate Descending (t a) where
   validate p x = do
     unless (decreasing x) $ do
-      throwRefineOtherException (typeOf p)
-        $ "Foldable is not in descending order "
+      throwRefineOtherException (typeOf p) ( "Foldable is not in descending order." )
 
 --------------------------------------------------------------------------------
 
@@ -490,8 +515,7 @@
   validate p x = do
     let x' = natVal p
     unless (x < fromIntegral x') $ do
-      throwRefineOtherException (typeOf p)
-        $ "Value is not less than " <> PP.pretty x'
+      throwRefineOtherException (typeOf p) ( "Value is not less than " <> PP.pretty x' )
 
 --------------------------------------------------------------------------------
 
@@ -504,8 +528,7 @@
   validate p x = do
     let x' = natVal p
     unless (x > fromIntegral x') $ do
-      throwRefineOtherException (typeOf p)
-        $ "Value is not greater than " <> PP.pretty x'
+      throwRefineOtherException (typeOf p) ( "Value is not greater than " <> PP.pretty x' )
 
 --------------------------------------------------------------------------------
 
@@ -518,8 +541,7 @@
   validate p x = do
     let x' = natVal p
     unless (x >= fromIntegral x') $ do
-      throwRefineOtherException (typeOf p)
-        $ "Value is less than " <> PP.pretty x'
+      throwRefineOtherException (typeOf p) ( "Value is less than " <> PP.pretty x' )
 
 --------------------------------------------------------------------------------
 
@@ -532,8 +554,7 @@
   validate p x = do
     let x' = natVal p
     unless (x <= fromIntegral x') $ do
-      throwRefineOtherException (typeOf p)
-        $ "Value is greater than " <> PP.pretty x'
+      throwRefineOtherException (typeOf p) ( "Value is greater than " <> PP.pretty x' )
 
 --------------------------------------------------------------------------------
 
@@ -566,8 +587,7 @@
   validate p x = do
     let x' = natVal p
     unless (x == fromIntegral x') $ do
-      throwRefineOtherException (typeOf p)
-        $ "Value does not equal " <> PP.pretty x'
+      throwRefineOtherException (typeOf p) ( "Value does not equal " <> PP.pretty x' )
 
 --------------------------------------------------------------------------------
 
@@ -580,11 +600,31 @@
   validate p x = do
     let x' = natVal p
     unless (x /= fromIntegral x') $ do
-      throwRefineOtherException (typeOf p)
-        $ "Value does equal " <> PP.pretty x'
+      throwRefineOtherException (typeOf p) ( "Value does equal " <> PP.pretty x' )
 
 --------------------------------------------------------------------------------
 
+-- | A 'Predicate' ensuring that the value is greater or equal than a negative
+--   number specified as a type-level (positive) number @n@ and less than a
+--   type-level (positive) number @m@.
+data NegativeFromTo (n :: Nat) (m :: Nat)
+  deriving (Generic)
+
+instance (Ord x, Num x, KnownNat n, KnownNat m, n <= m) => Predicate (NegativeFromTo n m) x where
+  validate p x = do
+    let n' = natVal (Proxy @n)
+        m' = natVal (Proxy @m)
+    unless (x >= negate (fromIntegral n') && x <= fromIntegral m') $ do
+      let msg = [ "Value is out of range (minimum: "
+                , PP.pretty (negate n')
+                , ", maximum: "
+                , PP.pretty m'
+                , ")"
+                ] |> mconcat
+      throwRefineOtherException (typeOf p) msg
+
+--------------------------------------------------------------------------------
+
 -- | A 'Predicate' ensuring that the value is greater than zero.
 type Positive = GreaterThan 0
 
@@ -680,6 +720,8 @@
     RefineNotException
     { _RefineException_typeRep   :: !TypeRep
       -- ^ The 'TypeRep' of the @'Not' p@ type.
+    , _RefineException_notChild  :: !RefineException
+      -- ^ The 'RefineException' for the @p@ failure.
     }
 
   | -- | A 'RefineException' for failures involving the 'And' predicate.
@@ -718,24 +760,61 @@
 instance Show RefineException where
   show = PP.pretty .> show
 
+twoSpaces, newline :: PP.Doc ann
+{-# INLINE twoSpaces #-}
+{-# INLINE newline   #-}
+twoSpaces = "  "
+newline = "\n"
+
 -- | Display a 'RefineException' as a @'PP.Doc' ann@
 displayRefineException :: RefineException -> PP.Doc ann
-displayRefineException (RefineOtherException tr msg)
-  = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t" ++ show msg)
-displayRefineException (RefineNotException tr)
-  = PP.pretty ("The negation of the predicate (" ++ show tr ++ ") does not hold.")
-displayRefineException (RefineOrException tr orLChild orRChild)
-  = PP.pretty ("Both subpredicates failed in: (" ++ show tr ++ "). \n")
-      <> "\t" <> (displayRefineException orLChild) <> "\n"
-      <> "\t" <> (displayRefineException orRChild) <> "\n"
-displayRefineException (RefineAndException tr andChild)
-  = PP.pretty ("The predicate (" ++ show tr ++ ") does not hold: \n \t")
-      <> case andChild of
-           This a -> "The left subpredicate does not hold:\n\t" <> displayRefineException a <> "\n"
-           That b -> "The right subpredicate does not hold:\n\t" <> displayRefineException b <> "\n"
-           These a b -> "\t Neither subpredicate holds: \n"
-             <> "\t" <> displayRefineException a <> "\n"
-             <> "\t" <> displayRefineException b <> "\n"
+displayRefineException = \case
+  RefineOtherException tr msg ->
+    [ "The predicate ("
+    , PP.pretty (show tr)
+    , ") does not hold: "
+    , newline
+    , twoSpaces
+    , PP.pretty (show msg)
+    ] |> mconcat
+  RefineNotException tr notChild ->
+    [ "The negation of the predicate ("
+    , PP.pretty (show tr)
+    , ") does not hold:"
+    , newline
+    , twoSpaces
+    , displayRefineException notChild
+    , newline
+    ] |> mconcat
+  RefineOrException tr orLChild orRChild ->
+    [ "Both subpredicates failed in: ("
+    , PP.pretty (show tr)
+    , "):"
+    , newline
+    , twoSpaces
+    , displayRefineException orLChild
+    , newline
+    , twoSpaces
+    , displayRefineException orRChild
+    , newline
+    , twoSpaces
+    ] |> mconcat
+  RefineAndException tr andChild ->
+    (
+      [ "The predicate ("
+      , PP.pretty (show tr)
+      , ") does not hold:"
+      , newline
+      , twoSpaces
+      ] |> mconcat
+    )
+    <> case andChild of
+         This a -> mconcat [ "The left subpredicate does not hold:", newline, twoSpaces, displayRefineException a, newline ]
+         That b -> mconcat [ "The right subpredicate does not hold:", newline, twoSpaces, displayRefineException b, newline ]
+         These a b -> mconcat [ twoSpaces, "Neither subpredicate holds: ", newline
+                              , twoSpaces, displayRefineException a, newline
+                              , twoSpaces, displayRefineException b, newline
+                              ]
 
 -- | Pretty-print a 'RefineException'.
 instance PP.Pretty RefineException where
@@ -783,7 +862,7 @@
 refineM
   :: Either RefineException a
   -> RefineM a
-refineM = ExceptT.except .> coerce
+refineM = ExceptT.except .> (coerce :: ExceptT RefineException Identity a -> RefineM a)
 
 -- | Run a monadic action of type @'RefineM' a@,
 --   yielding an @'Either' 'RefineException' a@.
diff --git a/library/Refined/Orphan.hs b/library/Refined/Orphan.hs
new file mode 100644
--- /dev/null
+++ b/library/Refined/Orphan.hs
@@ -0,0 +1,44 @@
+--------------------------------------------------------------------------------
+
+-- Copyright © 2015 Nikita Volkov
+-- Copyright © 2018 Remy Goldschmidt
+-- Copyright © 2018 Daniel Cartwright
+--
+-- Permission is hereby granted, free of charge, to any person
+-- obtaining a copy of this software and associated documentation
+-- files (the "Software"), to deal in the Software without
+-- restriction, including without limitation the rights to use,
+-- copy, modify, merge, publish, distribute, sublicense, and/or sell
+-- copies of the Software, and to permit persons to whom the
+-- Software is furnished to do so, subject to the following
+-- conditions:
+--
+-- The above copyright notice and this permission notice shall be
+-- included in all copies or substantial portions of the Software.
+--
+-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+-- OTHER DEALINGS IN THE SOFTWARE.
+
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE CPP #-}
+
+--------------------------------------------------------------------------------
+
+-- | This module exposes orphan instances for the 'Refined' type.
+--   This is unavoidable given the current module structure.
+module Refined.Orphan () where
+
+--------------------------------------------------------------------------------
+
+import Refined.Orphan.Aeson ()
+import Refined.Orphan.QuickCheck ()
+
+--------------------------------------------------------------------------------
+
diff --git a/library/Refined/Orphan/Aeson.hs b/library/Refined/Orphan/Aeson.hs
new file mode 100644
--- /dev/null
+++ b/library/Refined/Orphan/Aeson.hs
@@ -0,0 +1,56 @@
+--------------------------------------------------------------------------------
+
+-- Copyright © 2015 Nikita Volkov
+-- Copyright © 2018 Remy Goldschmidt
+-- Copyright © 2018 Daniel Cartwright
+--
+-- Permission is hereby granted, free of charge, to any person
+-- obtaining a copy of this software and associated documentation
+-- files (the "Software"), to deal in the Software without
+-- restriction, including without limitation the rights to use,
+-- copy, modify, merge, publish, distribute, sublicense, and/or sell
+-- copies of the Software, and to permit persons to whom the
+-- Software is furnished to do so, subject to the following
+-- conditions:
+--
+-- The above copyright notice and this permission notice shall be
+-- included in all copies or substantial portions of the Software.
+--
+-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+-- OTHER DEALINGS IN THE SOFTWARE.
+
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE CPP #-}
+
+--------------------------------------------------------------------------------
+
+-- | This module exposes orphan instances for the 'Refined' type.
+--   This is unavoidable given the current module structure.
+module Refined.Orphan.Aeson () where
+
+--------------------------------------------------------------------------------
+
+#if HAVE_AESON
+
+import           Control.Monad    ((<=<))
+import           Data.Aeson       (FromJSON(parseJSON), ToJSON(toJSON))            
+import           Refined.Internal (Refined, Predicate, refineFail, unrefine)
+
+--------------------------------------------------------------------------------
+
+instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where
+  parseJSON = refineFail <=< parseJSON
+
+instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where
+  toJSON = toJSON . unrefine
+
+--------------------------------------------------------------------------------
+
+#endif
diff --git a/library/Refined/Orphan/QuickCheck.hs b/library/Refined/Orphan/QuickCheck.hs
new file mode 100644
--- /dev/null
+++ b/library/Refined/Orphan/QuickCheck.hs
@@ -0,0 +1,54 @@
+--------------------------------------------------------------------------------
+
+-- Copyright © 2015 Nikita Volkov
+-- Copyright © 2018 Remy Goldschmidt
+-- Copyright © 2018 Daniel Cartwright
+--
+-- Permission is hereby granted, free of charge, to any person
+-- obtaining a copy of this software and associated documentation
+-- files (the "Software"), to deal in the Software without
+-- restriction, including without limitation the rights to use,
+-- copy, modify, merge, publish, distribute, sublicense, and/or sell
+-- copies of the Software, and to permit persons to whom the
+-- Software is furnished to do so, subject to the following
+-- conditions:
+--
+-- The above copyright notice and this permission notice shall be
+-- included in all copies or substantial portions of the Software.
+--
+-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+-- OTHER DEALINGS IN THE SOFTWARE.
+
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+--------------------------------------------------------------------------------
+
+-- | This module exposes orphan instances for the 'Refined' type.
+--   This is unavoidable given the current module structure.
+module Refined.Orphan.QuickCheck () where
+
+--------------------------------------------------------------------------------
+
+#if HAVE_QUICKCHECK
+
+import           Data.Either      (isRight)
+import           Refined.Internal (Refined(Refined), RefineException, Predicate, refine)
+import           Test.QuickCheck  (Arbitrary(arbitrary), suchThat, Gen)
+
+--------------------------------------------------------------------------------
+
+instance forall p a. (Arbitrary a, Predicate p a) => Arbitrary (Refined p a) where
+  arbitrary = Refined <$> suchThat (arbitrary :: Gen a) (isRight . (refine :: a -> Either RefineException (Refined p a)))
+
+--------------------------------------------------------------------------------
+
+#endif
diff --git a/library/Refined/These.hs b/library/Refined/These.hs
deleted file mode 100644
--- a/library/Refined/These.hs
+++ /dev/null
@@ -1,264 +0,0 @@
---------------------------------------------------------------------------------
-
--- Copyright © 2015 Nikita Volkov
--- Copyright © 2018 Remy Goldschmidt
--- Copyright © 2018 Daniel Cartwright
---
--- Permission is hereby granted, free of charge, to any person
--- obtaining a copy of this software and associated documentation
--- files (the "Software"), to deal in the Software without
--- restriction, including without limitation the rights to use,
--- copy, modify, merge, publish, distribute, sublicense, and/or sell
--- copies of the Software, and to permit persons to whom the
--- Software is furnished to do so, subject to the following
--- conditions:
---
--- The above copyright notice and this permission notice shall be
--- included in all copies or substantial portions of the Software.
---
--- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
--- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
--- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
--- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
--- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
--- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
--- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
--- OTHER DEALINGS IN THE SOFTWARE.
-
---------------------------------------------------------------------------------
-
-{-# OPTIONS_GHC -Wall #-}
-
---------------------------------------------------------------------------------
-
-{-# LANGUAGE CPP                #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveGeneric      #-}
-{-# LANGUAGE InstanceSigs       #-}
-
---------------------------------------------------------------------------------
-
--- | This module is defined internally to avoid using the 'these'
---   package, which brings in a lot of very heavy and unnecessary 
---   transitive dependencies. We export the type and constructors
---   here, in case a user should need it.
---   We provide a small API for working with the 'These' type here.
---   If one should need a fuller API, see https://hackage.haskell.org/package/these
---   Converting to/from the two types should be trivial, as the
---   data constructors are exported from both.
-module Refined.These
-  (
-    -- * 'These' type    
-    These(This, That, These)
-  
-    -- * Consumption
-  , these
-  , fromThese
-  , mergeThese
-  , mergeTheseWith
-
-    -- * Traversals
-  , here, there
-
-    -- * Case selections
-  , justThis
-  , justThat
-  , justThese
-
-  , catThis
-  , catThat
-  , catThese
-  
-  , partitionThese
-
-    -- * Case predicates
-  , isThis
-  , isThat
-  , isThese
-
-    -- * Map operations
-  , mapThese
-  , mapThis
-  , mapThat
-  ) where
-
---------------------------------------------------------------------------------
-
-import Control.DeepSeq (NFData(rnf))
-#if MIN_VERSION_base(4,10,0)
-import Data.Bifoldable (Bifoldable(bifold, bifoldr, bifoldl))
-#endif
-#if MIN_VERSION_base(4,8,0)
-import Data.Bifunctor  (Bifunctor(bimap, first, second))
-#endif
-import Data.Data       (Data)
-import Data.Maybe      (isJust, mapMaybe)
-import Data.Semigroup  (Semigroup((<>)))
-import Data.Typeable   (Typeable)
-import GHC.Generics    (Generic, Generic1)
- 
--- | This is defined internally to avoid using the 'these'
---   package, which brings in a lot of very heavy and unnecessary 
---   transitive dependencies. We export the type and constructors
---   here, in case a user should need it.
-data These a b = This a | That b | These a b
-  deriving (Eq, Ord, Read, Show, Typeable, Data, Generic, Generic1)
-
--- | Case analysis for the 'These' type.
-these :: (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
-these l _ _ (This a) = l a
-these _ r _ (That x) = r x
-these _ _ lr (These a x) = lr a x
-
--- | Takes two default values and produces a tuple.
-fromThese :: a -> b -> These a b -> (a, b)
-fromThese _ x (This a   ) = (a, x)
-fromThese a _ (That x   ) = (a, x)
-fromThese _ _ (These a x) = (a, x)
-
--- | Coalesce with the provided operation.
-mergeThese :: (a -> a -> a) -> These a a -> a
-mergeThese = these id id
-
--- | BiMap and coalesce results with the provided operation.
-mergeTheseWith :: (a -> c) -> (b -> c) -> (c -> c -> c) -> These a b -> c
-mergeTheseWith f g op t = mergeThese op $ mapThese f g t
-
--- | A @Traversal@ of the first half of a 'These', suitable for use with @Control.Lens@.
-here :: (Applicative f) => (a -> f b) -> These a t -> f (These b t)
-here f (This x) = This <$> f x
-here f (These x y) = flip These y <$> f x
-here _ (That x) = pure (That x)
-
--- | A @Traversal@ of the second half of a 'These', suitable for use with @Control.Lens@.
-there :: (Applicative f) => (a -> f b) -> These t a -> f (These t b)
-there _ (This x) = pure (This x)
-there f (These x y) = These x <$> f y
-there f (That x) = That <$> f x
-
--- | @'justThis' = 'these' 'Just' (\_ -> 'Nothing') (\_ _ -> 'Nothing')@
-justThis :: These a b -> Maybe a
-justThis = these Just (\_ -> Nothing) (\_ _ -> Nothing)
-
--- | @'justThat' = 'these' (\_ -> 'Nothing') 'Just' (\_ _ -> 'Nothing')@
-justThat :: These a b -> Maybe b
-justThat = these (\_ -> Nothing) Just (\_ _ -> Nothing)
-
--- | @'justThese' = 'these' (\_ -> 'Nothing') (\_ -> 'Nothing') (\a b -> 'Just' (a, b))@
-justThese :: These a b -> Maybe (a, b)
-justThese = these (\_ -> Nothing) (\_ -> Nothing) (\a b -> Just (a, b))
-
-isThis, isThat, isThese :: These a b -> Bool
--- | @'isThis' = 'isJust' . 'justThis'@
-isThis  = isJust . justThis
-
--- | @'isThat' = 'isJust' . 'justThat'@
-isThat  = isJust . justThat
-
--- | @'isThese' = 'isJust' . 'justThese'@
-isThese = isJust . justThese
-
--- | 'Bifunctor' map.
-mapThese :: (a -> c) -> (b -> d) -> These a b -> These c d
-mapThese f _ (This  a  ) = This (f a)
-mapThese _ g (That    x) = That (g x)
-mapThese f g (These a x) = These (f a) (g x)
-
--- | @'mapThis' = over 'here'@
-mapThis :: (a -> c) -> These a b -> These c b
-mapThis f = mapThese f id
-
--- | @'mapThat' = over 'there'@
-mapThat :: (b -> d) -> These a b -> These a d
-mapThat f = mapThese id f
-
--- | Select all 'This' constructors from a list.
-catThis :: [These a b] -> [a]
-catThis = mapMaybe justThis
-
--- | Select all 'That' constructors from a list.
-catThat :: [These a b] -> [b]
-catThat = mapMaybe justThat
-
--- | Select all 'These' constructors from a list.
-catThese :: [These a b] -> [(a, b)]
-catThese = mapMaybe justThese
-
--- | Select each constructor and partition them into separate lists.
-partitionThese :: [These a b] -> ( [(a, b)], ([a], [b]) )
-partitionThese []             = ([], ([], []))
-partitionThese (These x y:xs) = first ((x, y):)      $ partitionThese xs
-partitionThese (This  x  :xs) = second (first  (x:)) $ partitionThese xs
-partitionThese (That    y:xs) = second (second (y:)) $ partitionThese xs
-
-instance (Semigroup a, Semigroup b) => Semigroup (These a b) where
-    This  a   <> This  b   = This  (a <> b)
-    This  a   <> That    y = These  a             y
-    This  a   <> These b y = These (a <> b)       y
-    That    x <> This  b   = These       b   x
-    That    x <> That    y = That           (x <> y)
-    That    x <> These b y = These       b  (x <> y)
-    These a x <> This  b   = These (a <> b)  x
-    These a x <> That    y = These  a       (x <> y)
-    These a x <> These b y = These (a <> b) (x <> y)
-
-#if MIN_VERSION_base(4,8,0)
-instance Bifunctor These where
-  bimap :: (a -> c) -> (b -> d) -> These a b -> These c d 
-  bimap f _ (This a   ) = This  (f a)
-  bimap _ g (That    b) = That        (g b)
-  bimap f g (These a b) = These (f a) (g b)
-  first :: (a -> c) -> These a b -> These c b
-  first f = bimap f id
-  second :: (b -> d) -> These a b -> These a d
-  second f = bimap id f
-#endif
-
-instance Functor (These a) where
-    fmap _ (This x) = This x
-    fmap f (That y) = That (f y)
-    fmap f (These x y) = These x (f y)
-
-instance Semigroup a => Applicative (These a) where
-  pure = That
-  This  a   <*> _         = This a
-  That    _ <*> This  b   = This b
-  That    f <*> That    x = That (f x)
-  That    f <*> These b x = These b (f x)
-  These a _ <*> This  b   = This (a <> b)
-  These a f <*> That    x = These a (f x)
-  These a f <*> These b x = These (a <> b) (f x)
-
-instance Semigroup a => Monad (These a) where
-  return = pure
-  This  a   >>= _ = This a
-  That    x >>= k = k x
-  These a x >>= k = case k x of
-                        This  b   -> This  (a <> b)
-                        That    y -> These a y
-                        These b y -> These (a <> b) y
-
-instance (NFData a, NFData b) => NFData (These a b) where
-  rnf (This a) = rnf a
-  rnf (That b) = rnf b
-  rnf (These a b) = rnf a `seq` rnf b
-
-instance Foldable (These a) where
-    foldr _ z (This _) = z
-    foldr f z (That x) = f x z
-    foldr f z (These _ x) = f x z
-
-instance Traversable (These a) where
-    traverse _ (This  a  ) = pure $ This a
-    traverse f (That    x) = That <$> f x
-    traverse f (These a x) = These a <$> f x
-    sequenceA (This  a  ) = pure $ This a
-    sequenceA (That    x) = That <$> x
-    sequenceA (These a x) = These a <$> x
-
-#if MIN_VERSION_base(4,10,0)
-instance Bifoldable These where
-    bifold = these id id mappend
-    bifoldr f g z = these (`f` z) (`g` z) (\x y -> x `f` (y `g` z))
-    bifoldl f g z = these (z `f`) (z `g`) (\x y -> (z `f` x) `g` y)
-#endif
diff --git a/refined.cabal b/refined.cabal
--- a/refined.cabal
+++ b/refined.cabal
@@ -1,7 +1,9 @@
+cabal-version:
+  2.0
 name:
   refined
 version:
-  0.3.0.0
+  0.4
 synopsis:
   Refinement types with static and runtime checking
 description:
@@ -28,13 +30,28 @@
   LICENSE
 build-type:
   Simple
-cabal-version:
-  >=1.10
 tested-with:
     GHC == 8.0.2
   , GHC == 8.2.2
-  , GHC == 8.4.2
+  , GHC == 8.4.4
+  , GHC == 8.6.4
 
+flag aeson
+  description:
+    You can disable the use of the `aeson` package using `-f-aeson`.
+    .
+    This may be useful for accelerating builds in sandboxes for expert users.
+  default: True
+  manual: True
+
+flag QuickCheck
+  description:
+    You can disable the use of the `QuickCheck` package using `-f-QuickCheck`.
+    .
+    This may be useful for accelerating builds in sandboxes for expert users.
+  default: True
+  manual: True
+
 source-repository head
   type:
     git
@@ -47,16 +64,25 @@
   exposed-modules:
     Refined
     Refined.Internal
-    Refined.These
+    Refined.Orphan
+      Refined.Orphan.Aeson
+      Refined.Orphan.QuickCheck
     Refined.Unsafe 
-    Refined.Unsafe.Type
+      Refined.Unsafe.Type
   default-language:
     Haskell2010
   build-depends:
-      base >= 4.9 && < 5
-    , deepseq >= 1.4.0.0 
-    , exceptions >= 0.8.0
-    , mtl >= 2.2.1
-    , prettyprinter >= 1.1.0.1
-    , template-haskell >= 2.9 && < 3.0
-    , transformers >= 0.5.0.0
+      base             >= 4.9.1.0 && < 4.13.0.0
+    , deepseq          >= 1.4.0.0 && < 1.5.0.0
+    , exceptions       >= 0.8.0.0 && < 0.11.0
+    , mtl              >= 2.2.1.0 && < 3.0.0.0
+    , prettyprinter    >= 1.1.0.1 && < 1.3.0.0
+    , template-haskell >= 2.9.0.0 && < 2.15.0.0
+    , these            >= 0.7.0.0 && < 0.8.0.0
+    , transformers     >= 0.5.0.0 && < 0.6.0.0
+  if flag(aeson)
+    build-depends: aeson >= 0.9 && < 1.5.0.0
+    cpp-options: -DHAVE_AESON
+  if flag(QuickCheck)
+    build-depends: QuickCheck >= 2.1 && < 2.13
+    cpp-options: -DHAVE_QUICKCHECK