add refine_ and refineTH_

changelog.md

@@ -4,6 +4,11 @@ All notable changes to this project will be documented in this file.
 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/).
 
+## [???] - ???
+### Added
+- `refine_`
+- `refineTH_`
+
 ## [0.4.2.3] - 2019-09-17
 ### Added
 - `reifyPredicate`

refined.cabal

@@ -105,3 +105,12 @@ test-suite arbitrary
     , refined
     , QuickCheck
   default-language: Haskell2010
+
+test-suite compiles
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: Compiles.hs
+  build-depends:
+      base
+    , refined
+  default-language: Haskell2010

src/Refined.hs

@@ -58,10 +58,12 @@ module Refined
 
     -- ** Creation
   , refine
+  , refine_
   , refineThrow
   , refineFail
   , refineError
   , refineTH
+  , refineTH_
 
     -- ** Consumption
   , unrefine

src/Refined/Internal.hs

@@ -46,6 +46,7 @@
 {-# LANGUAGE MultiParamTypeClasses      #-}
 {-# LANGUAGE OverloadedStrings          #-}
 {-# LANGUAGE QuasiQuotes                #-}
+{-# LANGUAGE RankNTypes                 #-}
 {-# LANGUAGE RoleAnnotations            #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE TemplateHaskell            #-}
@@ -72,10 +73,12 @@ module Refined.Internal
 
     -- ** Creation
   , refine
+  , refine_
   , refineThrow
   , refineFail
   , refineError
   , refineTH
+  , refineTH_
 
     -- ** Consumption
   , unrefine
@@ -299,6 +302,13 @@ refine x = do
     pure (Refined x)
 {-# INLINABLE refine #-}
 
+-- | Like 'refine', but discards the refinement.
+--   This _can_ be useful when you only need to validate
+--   that some value at runtime satisfies some predicate.
+--   See also 'reifyPredicate'.
+refine_ :: forall p x. (Predicate p x) => x -> Either RefineException x
+refine_ = refine @p @x .> coerce
+
 -- | Constructs a 'Refined' value at run-time,
 --   calling 'Control.Monad.Catch.throwM' if the value
 --   does not satisfy the predicate.
@@ -356,6 +366,22 @@ refineTH =
        .> either (show .> fail) TH.lift
        .> fmap TH.TExp
 
+-- | Like 'refineTH', but immediately unrefines the value.
+--   This is useful when some value need only be refined
+--   at compile-time.
+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
+
 --------------------------------------------------------------------------------
 
 -- | Extracts the refined value.

test/Compiles.hs

@@ -0,0 +1,24 @@
+{-# language
+    AllowAmbiguousTypes
+  , TemplateHaskell
+  , TypeApplications
+  #-}
+
+module Main (main) where
+
+import Refined
+import Prelude (IO,putStrLn,Int)
+
+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)
+
+id_   = $$(refineTH_ @IdPred     @Int 3)
+even_ = $$(refineTH_ @(Not Even) @Int 3)
+odd_  = $$(refineTH_ @Odd        @Int 3)
+
+