diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -4,6 +4,11 @@
 The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
 and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## [0.5.1] - 2020-07-14
+### Changed
+- `refineTH_` is now implemented in terms of `refineTH`
+- Fix pretty-printing of `RefineException`s during compile-time
+
 ## [0.5] - 2020-07-11
 ### Added
 - sized Predicate instances for `Text`
diff --git a/refined.cabal b/refined.cabal
--- a/refined.cabal
+++ b/refined.cabal
@@ -3,7 +3,7 @@
 name:
   refined
 version:
-  0.5
+  0.5.1
 synopsis:
   Refinement types with static and runtime checking
 description:
diff --git a/src/Refined.hs b/src/Refined.hs
--- a/src/Refined.hs
+++ b/src/Refined.hs
@@ -46,6 +46,7 @@
 {-# LANGUAGE PackageImports             #-}
 {-# LANGUAGE RoleAnnotations            #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE TemplateHaskell            #-}
 {-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE TypeFamilies               #-}
 {-# LANGUAGE TypeOperators              #-}
@@ -411,8 +412,9 @@
         -> x
         -> Either RefineException (Refined p x)
       refineByResult = const refine
+      showException = refineExceptionToTree .> showTree True
   in fix $ \loop -> refineByResult (loop undefined)
-       .> either (show .> fail) TH.lift
+       .> either (showException .> show .> fail) TH.lift
        .> fmap TH.TExp
 
 -- | Like 'refineTH', but immediately unrefines the value.
@@ -423,16 +425,12 @@
 refineTH_ :: forall p x. (Predicate p x, TH.Lift x)
   => x
   -> TH.Q (TH.TExp x)
-refineTH_ =
-  let refineByResult :: (Predicate p x)
-        => TH.Q (TH.TExp x)
-        -> x
-        -> Either RefineException x
-      refineByResult = const (refine_ @p @x)
-  in fix $ \loop -> refineByResult (loop undefined)
-       .> either (show .> fail) TH.lift
-       .> fmap TH.TExp
+refineTH_ = refineTH @p @x .> fmap unsafeUnrefineTExp
 
+unsafeUnrefineTExp :: TH.TExp (Refined p x) -> TH.TExp x
+unsafeUnrefineTExp (TH.TExp e) = TH.TExp
+  (TH.VarE 'unrefine `TH.AppE` e)
+
 --------------------------------------------------------------------------------
 
 -- | Extracts the refined value.
@@ -1409,6 +1407,8 @@
 instance Show RefineException where
   show = PP.pretty .> show
 
+-- | A Tree which is a bit easier to pretty-print
+--   TODO: get rid of this
 data ExceptionTree a
   = NodeNone
   | NodeSome !TypeRep SomeException
@@ -1418,9 +1418,26 @@
   | NodeAnd !TypeRep [ExceptionTree a]
   | NodeXor !TypeRep [ExceptionTree a]
 
-showTree :: ExceptionTree RefineException -> PP.Doc ann
-showTree = PP.pretty . unlines . showOne "  " "" ""
+-- | pretty-print an 'ExceptionTree', contains a hack to
+--   work differently whether or not you are "inGhc", i.e.
+--   inside of refineTH/refineTH_ (because GHC messes with
+--   the indentation)
+showTree :: Bool -> ExceptionTree RefineException -> PP.Doc ann
+showTree inGhc
+  | inGhc = showOne "" "" ""
+      .> mapOnTail (indent 6)
+      .> unlines
+      .> PP.pretty
+  | otherwise = showOne "  " "" "" .> unlines .> PP.pretty
   where
+    mapOnTail :: (a -> a) -> [a] -> [a]
+    mapOnTail f = \case
+      [] -> []
+      (a : as) -> a : map f as
+
+    indent :: Int -> String -> String
+    indent n s = replicate n ' ' ++ s
+
     showOne :: String -> String -> String -> ExceptionTree RefineException -> [String]
     showOne leader tie arm = \case
       NodeNone ->
@@ -1434,7 +1451,6 @@
           <> show tr
           <> ") failed with the exception: "
           <> displayException e
-          <> "."
         ]
       NodeOther tr p ->
         [ leader
@@ -1444,7 +1460,6 @@
           <> show tr
           <> ") failed with the message: "
           <> show p
-          <> "."
         ]
       NodeNot tr ->
         [ leader
@@ -1452,7 +1467,7 @@
           <> tie
           <> "The predicate ("
           <> show tr
-          <> ") does not hold."
+          <> ") does not hold"
         ]
       NodeOr tr rest -> nodeRep tr : showChildren rest (leader <> extension)
       NodeAnd tr rest -> nodeRep tr : showChildren rest (leader <> extension)
@@ -1463,7 +1478,7 @@
           <> tie
           <> "The predicate ("
           <> show tr
-          <> ") does not hold, because both predicates were satisfied."
+          <> ") does not hold, because both predicates were satisfied"
         ]
       NodeXor tr rest -> nodeRep tr : showChildren rest (leader <> extension)
       where
@@ -1535,7 +1550,7 @@
 --
 --   @since 0.2.0.0
 displayRefineException :: RefineException -> PP.Doc ann
-displayRefineException = refineExceptionToTree .> showTree
+displayRefineException = refineExceptionToTree .> showTree False
 
 -- | Pretty-print a 'RefineException'.
 --
diff --git a/test/Compiles.hs b/test/Compiles.hs
--- a/test/Compiles.hs
+++ b/test/Compiles.hs
@@ -1,5 +1,6 @@
 {-# language
     AllowAmbiguousTypes
+  , DataKinds
   , FlexibleInstances
   , MultiParamTypeClasses
   , OverloadedStrings
@@ -12,10 +13,33 @@
 import Refined
 import Data.Void (Void)
 
-main :: IO ()
-main = do
-  putStrLn "refined/test/Compiles.hs: it compiles!"
-
 id_   = $$(refineTH_ @IdPred     @Int 3)
 even_ = $$(refineTH_ @(Not Even) @Int 3)
 odd_  = $$(refineTH_ @Odd        @Int 3)
+
+--foo = $$(refineTH
+--        @( And
+--             Even
+--             ( Xor
+--                 ( And
+--                     (Not (DivisibleBy 3))
+--                     IdPred
+--                 )
+--                 (DivisibleBy 2)
+--             )
+--         )
+--        @Int
+--        3)
+--bar = case foo of
+--  Left e -> e
+--  Right _ -> error "bad!"
+
+main :: IO ()
+main = do
+  putStrLn "refined/test/Compiles.hs: it compiles!"
+  foldMap print
+    [ id_
+    , even_
+    , odd_
+    ]
+--  print bar