refined 0.4.4 → 0.5

raw patch · 15 files changed

+1872/−1757 lines, 15 filesdep +bytestringdep +textdep +these-skinnydep −transformersdep ~aesondep ~basedep ~mtl

Dependencies added: bytestring, text, these-skinny

Dependencies removed: transformers

Dependency ranges changed: aeson, base, mtl, template-haskell

Files

• LICENSE +1/−1
• README.md +13/−0
• changelog.md +144/−0
• refined.cabal +17/−16
• src/Refined.hs +1631/−146
• src/Refined/Internal.hs +0/−1150
• src/Refined/Orphan.hs +0/−44
• src/Refined/Orphan/Aeson.hs +0/−56
• src/Refined/Orphan/QuickCheck.hs +0/−91
• src/Refined/These.hs +9/−228
• src/Refined/Unsafe.hs +19/−11
• src/Refined/Unsafe/Type.hs +38/−4
• test/Compiles.hs +0/−5
• test/Doctests.hs +0/−4
• test/QuickCheck.hs +0/−1

@@ -1,6 +1,6 @@ Copyright © 2015 Nikita Volkov Copyright © 2018 Remy Goldschmidt-Copyright © 2019 chessai+Copyright © 2020 chessai  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation

@@ -0,0 +1,13 @@+# refined++[![Build Status](https://travis-ci.org/nikita-volkov/refined.svg?branch=master)](https://travis-ci.org/nikita-volkov/refined)++In type theory, a refinement type is a type endowed+with a predicate which is assumed to hold for any element+of the refined type.++This library allows one to capture the idea of a refinement type+using the `Refined` type. A `Refined` `p` `x` wraps a value+of type `x`, ensuring that it satisfies a type-level predicate `p`.++A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/

@@ -0,0 +1,144 @@+# Changelog+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/).++## [0.5] - 2020-07-11+### Added+- sized Predicate instances for `Text`+- sized Predicate instances for strict and lazy `ByteString`+- INLINABLE pragmas on `refine_` `reifyPredicate` +- `NFData` instance for `Refined`+- RefineSomeException constructor. Enables recovering+  specific validation exceptions.+  Thanks to @haroldcarr for adding this.+- RefineXorException constructor.+- `Empty` and `NotEmpty` predicates.+- `NaN` and `Infinite` predicates for floating-point numbers.+- @since pragmas to EVERYTHING.++### Changed+- lower bound on mtl to 2.2.2 due to use of liftEither. +  Thanks to @k0ral for reporting this+- Generalize sized predicates+- Allow newer template-haskell (< 0.16 ==> < 0.17)+- Allow newer aeson (< 1.5 ==> < 1.6)+  Thanks to @locallycompact for this change.++### Removed+- `Refined.Internal` module+  Thanks to @nikita-volkov for pushing me to do this.+- Orphan modules+  Thanks to @symbiont-sam-halliday for pointing out the+  silliness of these modules.+- `RefineT`. It was a needless abstraction that just made the+  library harder to learn and use, providing little benefit+  over `Maybe RefineException`.+  Thanks to @nikita-volkov for helping me see the light.++### Deprecated+- Refined.These module in favour of Data.These from these-skinny++## [0.4.4] - 2019-10-18+### Added+- `refine_`+- `refineTH_`+- test suite: unit tests for compiling.+### Changed+- Allow newer `template-haskell` and `QuickCheck`.++## [0.4.2.3] - 2019-09-17+### Added+- `reifyPredicate`+### Fixed+- `Arbitrary` instance for `Refined` should now always terminate.+   Thanks to @symbiont-joseph-kachmar for reporting this.++## [0.4.2.2] - 2019-07-19+### Added+- `exceptRefine`, `strengthen`, and `strengthenM`++## [0.4.2.1] - 2019-05-31+### Fixed+- Documentation fix for `DivisibleBy`+### Changed+- Re-export `DivisibleBy`, `Even`, and `Odd` from module `Refined`.+- Re-export all constructors from module `Refined`.++## [0.4.2] - 2019-05-30+### Removed+- Re-removed dependency of `these` package.+### Added+- `Even`, `Odd`, and `DivisibleBy` predicates.+- doctests for all predicates.+### Changed+- Make all predicates unary data constructors, instead of nullary,+  and export those newly added constructors.++## [0.4.1] - 2019-04-15+### Fixed+- Serious regression where `Not p` ~ `p`. Thanks to @k0ral who reported this.++## [0.4] - 2019-03-18+### Added+- 'NegativeFromTo', a Predicate that ensures a numeric value is within a range [a,b],+  where a < 0 and b >= a.+  Thanks to github.com/futtetennista for this change.+### Changed+- `RefinedNotException` now has a child (it should have had one in v2. This was an oversight.)+- `displayRefineException` no longer uses tabs, instead 2 spaces.+- make implementation of `displayRefineException` more clear via formatting.++## [0.3.0.0] - 2018-09-26+### Added+- Internal module, and Unsafe modules, making sure to take care w.r.t.+  the scope of coercions related to the use of the 'Refined' constructor.+- 'IdPred' predicate, predicate that never fails.+- Generic instances for all predicates.+- `reallyUnsafeRefine`, `reallyUnsafeUnderlyingRefined`, `reallyUnsafeAllUnderlyingRefined`,+  functions that allow one to use 'Coercion's to manually prove things about 'Refined'+  values.+### Changed+- Type role of Refined from 'phantom Representational' to 'nominal nominal'.+  With the old type role, one can use `coerce` to prove `Q x` given any `P x`.+  The second parameter should also be nominal because of interactions with something+  like `GreaterThan` and `Data.Ord.Down`.+  Thanks to David Feuer for pointing this out.+- Change docs to point users to 'Refined.Unsafe' module instead of recommending+  'Unsafe.Coerce.unsafeCoerce'.+- 'Ascending' and 'Descending' predicates now use 'Foldable' instead of 'IsList'.+- Lowered the lower bound on 'exceptions'; it was too strict for the support window.+### Removed+- Dependency of the 'these' package. It brings in some very+  heavy transitive dependencies, even though the datatype+  in `refined` is used to the most minimal extent.+  This is a breaking change because+  this change is exposed to the end user via 'RefineAndException'.+  It is exported from a module called 'Refined.These'. Users+  wishing to interact with such exceptions can either just+  use the datatype constituting a minimal API there, or depend+  on the 'these' package.++## [0.2.3.0] - 2018-06-01+### Added+- back in the 'Foldable' instance for 'Refined'. It is safe.++## [0.2.2.0] - 2018-05-31+### Removed+- Unsafe typeclass instances that could break the 'Refined' invariant.+  These should not have been added.++## [0.2.1.0] - 2018-05-31+### Removed+- Unsafe typeclass instances that could break the 'Refined' invariant.+  These should not have been added.++## [0.2.0.0] - 2018-05-30+### Changed+- Radical rewrite of the library, centred around 'RefineException'+  and the 'RefineT' monad transformer.+  'validate' now has the type signature+  validate :: (Predicate p x, Monad m) => p -> x -> RefineT m ()+### Added+- More predicates

@@ -3,7 +3,7 @@ name:   refined version:-  0.4.4+  0.5 synopsis:   Refinement types with static and runtime checking description:@@ -22,7 +22,7 @@ copyright:   Copyright © 2015, Nikita Volkov   Copyright © 2018, Remy Goldschmidt-  Copyright © 2019, chessai+  Copyright © 2020, chessai license:   MIT license-file:@@ -30,10 +30,13 @@ build-type:   Simple tested-with:-    GHC == 8.0.2-  , GHC == 8.2.2-  , GHC == 8.4.4+    GHC == 8.4.4   , GHC == 8.6.5+  , GHC == 8.8.3+  , GHC == 8.10.1+extra-source-files:+    README.md+  , changelog.md  flag aeson   description:@@ -62,25 +65,23 @@     src   exposed-modules:     Refined-    Refined.Internal-    Refined.Orphan-      Refined.Orphan.Aeson-      Refined.Orphan.QuickCheck     Refined.These     Refined.Unsafe       Refined.Unsafe.Type   default-language:     Haskell2010   build-depends:-      base             >= 4.9.1 && < 4.14+      base             >= 4.11 && < 4.15+    , bytestring       >= 0.10 && < 0.11     , deepseq          >= 1.4 && < 1.5     , exceptions       >= 0.8 && < 0.11-    , mtl              >= 2.2.1 && < 2.3-    , prettyprinter    >= 1.1.0.1 && < 1.4-    , template-haskell >= 2.9 && < 2.16-    , transformers     >= 0.5 && < 0.6+    , mtl              >= 2.2.2 && < 2.3+    , prettyprinter    >= 1.1.0.1 && < 1.7+    , template-haskell >= 2.9 && < 2.17+    , text             >= 1.2 && < 1.3+    , these-skinny     >= 0.7.4 && < 0.8   if flag(aeson)-    build-depends: aeson >= 0.9 && < 1.5+    build-depends: aeson >= 0.9 && < 1.6     cpp-options: -DHAVE_AESON   if flag(QuickCheck)     build-depends: QuickCheck >= 2.1 && < 2.14@@ -115,7 +116,7 @@     , refined   default-language: Haskell2010 --- test-suite doesnt-compile+--test-suite doesnt-compile --   type: exitcode-stdio-1.0 --   hs-source-dirs: test --   main-is: DoesntCompile.hs

@@ -2,149 +2,1634 @@  -- Copyright © 2015 Nikita Volkov -- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai------ 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 ExplicitNamespaces #-}-------------------------------------------------------------------------------------- | In type theory, a refinement type is a type endowed---   with a predicate which is assumed to hold for any element---   of the refined type.------   This library allows one to capture the idea of a refinement type---   using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value---   of type @x@, ensuring that it satisfies a type-level predicate @p@.------   A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/------   This module only provides /safe/ constructions of 'Refined'---   values, /safe/ meaning that the refinement predicate holds,---   and the construction of the 'Refined' value is total.------   If you can manually prove that the refinement predicate holds,---   or you do not necessarily care about this definition of safety,---   use the module /Refined.Unsafe/.-module Refined-  ( -- * 'Refined'-    Refined--    -- ** Creation-  , refine-  , refine_-  , refineThrow-  , refineFail-  , refineError-  , refineTH-  , refineTH_--    -- ** Consumption-  , unrefine--    -- * 'Predicate'-  , Predicate (validate)-  , reifyPredicate--    -- * Logical predicates-  , Not(..)-  , And(..)-  , type (&&)-  , Or(..)-  , type (||)--    -- * Identity predicate-  , IdPred(..)--    -- * Numeric predicates-  , LessThan(..)-  , GreaterThan(..)-  , From(..)-  , To(..)-  , FromTo(..)-  , NegativeFromTo(..)-  , EqualTo(..)-  , NotEqualTo(..)-  , Odd(..)-  , Even(..)-  , DivisibleBy(..)-  , Positive-  , NonPositive-  , Negative-  , NonNegative-  , ZeroToOne-  , NonZero--    -- * Foldable predicates-  , SizeLessThan(..)-  , SizeGreaterThan(..)-  , SizeEqualTo(..)-  , NonEmpty--    -- * IsList predicates-  , Ascending(..)-  , Descending(..)--    -- * Weakening-  , Weaken (weaken)-  , andLeft-  , andRight-  , leftOr-  , rightOr--    -- * Strengthening-  , strengthen-  , strengthenM--    -- * Error handling--    -- ** 'RefineException'-  , RefineException-    ( RefineNotException-    , RefineAndException-    , RefineOrException-    , RefineOtherException-    )-  , displayRefineException--    -- ** 'RefineT' and 'RefineM'-  , RefineT, runRefineT, exceptRefine, mapRefineT-  , RefineM, refineM, runRefineM-  , throwRefine, catchRefine-  , throwRefineOtherException--    -- * Re-Exports-  , pretty-  ) where------------------------------------------------------------------------------------import Refined.Internal---------------------------------------------------------------------------------+-- Copyright © 2020 chessai+--+-- 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                        #-}+{-# OPTIONS_GHC -fno-warn-orphans            #-}+{-# OPTIONS_GHC -funbox-strict-fields        #-}++--------------------------------------------------------------------------------++{-# LANGUAGE AllowAmbiguousTypes        #-}+{-# LANGUAGE BangPatterns               #-}+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE LambdaCase                 #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE OverloadedStrings          #-}+{-# LANGUAGE PackageImports             #-}+{-# LANGUAGE RoleAnnotations            #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE TypeOperators              #-}++--------------------------------------------------------------------------------++-- | In type theory, a refinement type is a type endowed+--   with a predicate which is assumed to hold for any element+--   of the refined type.+--+--   This library allows one to capture the idea of a refinement type+--   using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value+--   of type @x@, ensuring that it satisfies a type-level predicate @p@.+--+--   A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/+--+module Refined+  ( -- * 'Refined' type+    Refined++    -- ** Creation+  , refine+  , refine_+  , refineThrow+  , refineFail+  , refineError+  , refineTH+  , refineTH_++    -- ** Consumption+  , unrefine++    -- * 'Predicate'+  , Predicate (validate)+  , reifyPredicate++    -- * Logical predicates+  , Not(..)+  , And(..)+  , type (&&)+  , Or(..)+  , type (||)+  , Xor(..)++    -- * Identity predicate+  , IdPred(..)++    -- * Numeric predicates+  , LessThan(..)+  , GreaterThan(..)+  , From(..)+  , To(..)+  , FromTo(..)+  , NegativeFromTo(..)+  , EqualTo(..)+  , NotEqualTo(..)+  , Odd(..)+  , Even(..)+  , DivisibleBy(..)+  , NaN(..)+  , Infinite(..)+  , Positive+  , NonPositive+  , Negative+  , NonNegative+  , ZeroToOne+  , NonZero++    -- * Foldable predicates+    -- ** Size predicates+  , SizeLessThan(..)+  , SizeGreaterThan(..)+  , SizeEqualTo(..)+  , Empty+  , NonEmpty+    -- ** Ordering predicates+  , Ascending(..)+  , Descending(..)++    -- * Weakening+  , Weaken (weaken)+  , andLeft+  , andRight+  , leftOr+  , rightOr++    -- * Strengthening+  , strengthen++    -- * Error handling++    -- ** 'RefineException'+  , RefineException+    ( RefineNotException+    , RefineAndException+    , RefineOrException+    , RefineXorException+    , RefineOtherException+    , RefineSomeException+    )+  , displayRefineException++    -- ** 'validate' helpers+  , throwRefineOtherException+  , throwRefineSomeException+  , success++    -- * Re-Exports+  , PP.pretty+ ) where++--------------------------------------------------------------------------------++import           Control.Exception            (Exception (displayException))+import           Data.Coerce                  (coerce)+import           Data.Either                  (isRight)+import           Data.Foldable                (foldl')+import           Data.Function                (fix)+import           Data.Proxy                   (Proxy(Proxy))+import           Data.Text                    (Text)+import qualified Data.Text                    as Text+import qualified Data.ByteString              as BS+import qualified Data.ByteString.Lazy         as BL+import           Data.Typeable                (TypeRep, Typeable, typeOf)+import           Data.Void                    (Void)++import           Control.Monad.Catch          (MonadThrow, SomeException)+import qualified Control.Monad.Catch          as MonadThrow+import           Control.Monad.Error.Class    (MonadError)+import qualified Control.Monad.Error.Class    as MonadError+#if !MIN_VERSION_base(4,13,0)+import           Control.Monad.Fail           (MonadFail, fail)+import           Prelude                      hiding (fail)+#endif++import           GHC.Generics                 (Generic, Generic1)+import           GHC.TypeLits                 (type (<=), KnownNat, Nat, natVal)++import           Refined.Unsafe.Type          (Refined(Refined))++import qualified Data.Text.Prettyprint.Doc    as PP+import qualified Language.Haskell.TH.Syntax   as TH++#if HAVE_AESON+import           Control.Monad    ((<=<))+import           Data.Aeson       (FromJSON(parseJSON), ToJSON(toJSON))+#endif++#if HAVE_QUICKCHECK+import           Test.QuickCheck  (Arbitrary, Gen)+import qualified Test.QuickCheck  as QC+import           Data.Typeable    (showsTypeRep, typeRep)+#endif++import "these-skinny" Data.These                   (These(This,That,These))++--------------------------------------------------------------------------------++-- $setup+--+-- Doctest imports+--+-- >>> :set -XDataKinds+-- >>> :set -XOverloadedStrings+-- >>> :set -XTypeApplications+-- >>> import Data.Int+-- >>> import Data.Either (isLeft)+--++--------------------------------------------------------------------------------++infixl 0 |>+infixl 9 .>++-- | Helper function, stolen from the flow package.+(|>) :: a -> (a -> b) -> b+(|>) = flip ($)+{-# INLINE (|>) #-}++-- | Helper function, stolen from the flow package.+(.>) :: (a -> b) -> (b -> c) -> a -> c+f .> g = \x -> g (f x)+{-# INLINE (.>) #-}++-- | FIXME: doc+data Ordered a = Empty | Decreasing a | Increasing a++-- | FIXME: doc+inc :: Ordered a -> Bool+inc (Decreasing _) = False+inc _              = True+{-# INLINE inc #-}++-- | FIXME: doc+dec :: Ordered a -> Bool+dec (Increasing _) = False+dec _              = True+{-# INLINE dec #-}++increasing :: (Foldable t, Ord a) => t a -> Bool+increasing = inc . foldl' go Empty where+  go Empty y = Increasing y+  go (Decreasing x) _ = Decreasing x+  go (Increasing x) y+    | x <= y = Increasing y+    | otherwise = Decreasing y+{-# INLINABLE increasing #-}++decreasing :: (Foldable t, Ord a) => t a -> Bool+decreasing = dec . foldl' go Empty where+  go Empty y = Decreasing y+  go (Increasing x) _ = Increasing x+  go (Decreasing x) y+    | x >= y = Decreasing y+    | otherwise = Increasing y+{-# INLINABLE decreasing #-}++--------------------------------------------------------------------------------++-- | This instance makes sure to check the refinement.+--+--   @since 0.1.0.0+instance (Read x, Predicate p x) => Read (Refined p x) where+  readsPrec d = readParen (d > 10) $ \r1 -> do+    ("Refined", r2) <- lex r1+    (raw,       r3) <- readsPrec 11 r2+    case refine raw of+      Right val -> [(val, r3)]+      Left  _   -> []++#if HAVE_AESON+-- | @since 0.4+instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where+  parseJSON = refineFail <=< parseJSON++-- | @since 0.4+instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where+  toJSON = toJSON . unrefine+#endif /* HAVE_AESON */++#if HAVE_QUICKCHECK+-- | @since 0.4+instance forall p a. (Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) where+  arbitrary = loop 0 QC.arbitrary+    where+      loop :: Int -> Gen a -> Gen (Refined p a)+      loop !runs gen+        | runs < 100 = do+            m <- suchThatRefined gen+            case m of+              Just x -> do+                pure x+              Nothing -> do+                loop (runs + 1) gen+        | otherwise = error (refinedGenError (Proxy @p) (Proxy @a))++refinedGenError :: (Typeable p, Typeable a)+  => Proxy p -> Proxy a -> String+refinedGenError p a = "arbitrary :: Refined ("+  ++ typeName p+  ++ ") ("+  ++ typeName a+  ++ "): Failed to generate a value that satisfied"+  ++ " the predicate after 100 tries."++suchThatRefined :: forall p a. (Predicate p a)+  => Gen a -> Gen (Maybe (Refined p a))+suchThatRefined gen = do+  m <- QC.suchThatMaybe gen (reifyPredicate @p @a)+  case m of+    Nothing -> pure Nothing+    Just x -> pure (Just (Refined x))++typeName :: Typeable a => Proxy a -> String+typeName = flip showsTypeRep "" . typeRep+#endif /* HAVE_QUICKCHECK */++--------------------------------------------------------------------------------++-- | A smart constructor of a 'Refined' value.+--   Checks the input value at runtime.+--+--   @since 0.1.0.0+refine :: (Predicate p x) => x -> Either RefineException (Refined p x)+refine x = do+  let predicateByResult :: Either RefineException (Refined p x) -> p+      predicateByResult = const undefined+  fix $ \result -> do+    maybe (Right (Refined x)) Left+      (validate (predicateByResult result) 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'.+--+--   @since 0.4.4+refine_ :: forall p x. (Predicate p x) => x -> Either RefineException x+refine_ = refine @p @x .> coerce+{-# INLINABLE refine_ #-}++-- | Constructs a 'Refined' value at run-time,+--   calling 'Control.Monad.Catch.throwM' if the value+--   does not satisfy the predicate.+--+--   @since 0.2.0.0+refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)+refineThrow = refine .> either MonadThrow.throwM pure+{-# INLINABLE refineThrow #-}++-- | Constructs a 'Refined' value at run-time,+--   calling 'Control.Monad.Fail.fail' if the value+--   does not satisfy the predicate.+--+--   @since 0.2.0.0+refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)+refineFail = refine .> either (displayException .> fail) pure+{-# INLINABLE refineFail #-}++-- | Constructs a 'Refined' value at run-time,+--   calling 'Control.Monad.Error.throwError' if the value+--   does not satisfy the predicate.+--+--   @since 0.2.0.0+refineError :: (Predicate p x, MonadError RefineException m)+            => x -> m (Refined p x)+refineError = refine .> either MonadError.throwError pure+{-# INLINABLE refineError #-}++--------------------------------------------------------------------------------++-- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@.+--+--   For example:+--+--   > $$(refineTH 23) :: Refined Positive Int+--   > Refined 23+--+--   Here's an example of an invalid value:+--+--   > $$(refineTH 0) :: Refined Positive Int+--   > <interactive>:6:4:+--   >     Value is not greater than 0+--   >     In the Template Haskell splice $$(refineTH 0)+--   >     In the expression: $$(refineTH 0) :: Refined Positive Int+--   >     In an equation for ‘it’:+--   >         it = $$(refineTH 0) :: Refined Positive Int+--+--   The example above indicates a compile-time failure,+--   which means that the checking was done at compile-time,+--   thus introducing a zero-runtime overhead compared to+--   a plain value construction.+--+--   /Note/: It may be useful to use this function with the+--   <https://hackage.haskell.org/package/th-lift-instances/ th-lift-instances package>.+--+--   @since 0.1.0.0+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++-- | Like 'refineTH', but immediately unrefines the value.+--   This is useful when some value need only be refined+--   at compile-time.+--+--   @since 0.4.4+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.+--+--   @since 0.1.0.0+unrefine :: Refined p x -> x+unrefine = coerce+{-# INLINE unrefine #-}++--------------------------------------------------------------------------------++-- | A typeclass which defines a runtime interpretation of+--   a type-level predicate @p@ for type @x@.+--+--   @since 0.1.0.0+class (Typeable p) => Predicate p x where+  {-# MINIMAL validate #-}+  -- | Check the value @x@ according to the predicate @p@,+  --   producing an error 'RefineException' if the value+  --   does not satisfy.+  --+  --   /Note/: 'validate' is not intended to be used+  --   directly; instead, it is intended to provide the minimal+  --   means necessary for other utilities to be derived. As+  --   such, the 'Maybe' here should be interpreted to mean+  --   the presence or absence of a 'RefineException', and+  --   nothing else.+  --+  --   /Note/: An implementation of 'validate' should not+  --   case on its first argument, @p@. This is due to an+  --   implementation detail of the 'refine' function. See+  --   <https://github.com/nikita-volkov/refined/issues/56 this issue>+  --   for more details.+  --+  --   @since 0.1.0.0+  validate :: p -> x -> Maybe RefineException++--------------------------------------------------------------------------------++-- | Reify a 'Predicate' by turning it into a value-level predicate.+--+--   @since 0.4.2.3+reifyPredicate :: forall p a. Predicate p a => a -> Bool+reifyPredicate = refine @p @a .> isRight+{-# INLINABLE reifyPredicate #-}++--------------------------------------------------------------------------------++-- | A predicate which is satisfied for all types.+--   Arguments passed to @'validate'@ in @'validate' 'IdPred' x@+--   are not evaluated.+--+--   >>> isRight (refine @IdPred @Int undefined)+--   True+--+--   >>> isLeft (refine @IdPred @Int undefined)+--   False+--+--   @since 0.3.0.0+data IdPred+  = IdPred -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.3.0.0+instance Predicate IdPred x where+  validate _ _ = Nothing+  {-# INLINE validate #-}++--------------------------------------------------------------------------------++-- | The negation of a predicate.+--+--   >>> isRight (refine @(Not NonEmpty) @[Int] [])+--   True+--+--   >>> isLeft (refine @(Not NonEmpty) @[Int] [1,2])+--   True+--+--   @since 0.1.0.0+data Not p+  = Not -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    , Generic1 -- ^ @since 0.3.0.0+    )++-- | @since 0.1.0.0+instance (Predicate p x, Typeable p) => Predicate (Not p) x where+  validate p x = do+    maybe (Just (RefineNotException (typeOf p)))+          (const Nothing)+          (validate @p undefined x)++--------------------------------------------------------------------------------++-- | The conjunction of two predicates.+--+--   >>> isLeft (refine @(And Positive Negative) @Int 3)+--   True+--+--   >>> isRight (refine @(And Positive Odd) @Int 203)+--   True+--+--   @since 0.1.0.0+data And l r+  = And -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    , Generic1 -- ^ @since 0.3.0.0+    )++infixr 3 &&+-- | The conjunction of two predicates.+--+--   @since 0.2.0.0+type (&&) = And++-- | @since 0.1.0.0+instance ( Predicate l x, Predicate r x, Typeable l, Typeable r+         ) => Predicate (And l r) x where+  validate p x = do+    let a = validate @l undefined x+    let b = validate @r undefined x+    let throw err = Just (RefineAndException (typeOf p) err)+    case (a, b) of+      (Just  e, Just e1) -> throw (These e e1)+      (Just  e,       _) -> throw (This e)+      (Nothing, Just  e) -> throw (That e)+      (Nothing, Nothing) -> Nothing++--------------------------------------------------------------------------------++-- | The disjunction of two predicates.+--+--   >>> isRight (refine @(Or Even Odd) @Int 3)+--   True+--+--   >>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)+--   True+--+--   >>> isRight (refine @(Or Even Even) @Int 4)+--   True+--+--   @since 0.1.0.0+data Or l r+  = Or -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    , Generic1 -- ^ @since 0.3.0.0+    )++infixr 2 ||+-- | The disjunction of two predicates.+--+--   @since 0.2.0.0+type (||) = Or++-- | @since 0.2.0.0+instance ( Predicate l x, Predicate r x, Typeable l, Typeable r+         ) => Predicate (Or l r) x where+  validate p x = do+    let left  = validate @l undefined x+    let right = validate @r undefined x+    case (left, right) of+      (Just l, Just r) -> Just (RefineOrException (typeOf p) l r)+      _                -> Nothing++--------------------------------------------------------------------------------++-- | The exclusive disjunction of two predicates.+--+--+--   >>> isRight (refine @(Xor Even Odd) @Int 3)+--   True+--+--   >>> isLeft (refine @(Xor (LessThan 3) (EqualTo 2)) @Int 2)+--   True+--+--   >>> isLeft (refine @(Xor Even Even) @Int 2)+--   True+--+--   @since 0.5+data Xor l r+  = Xor -- ^ @since 0.5+  deriving+    ( Generic -- ^ @since 0.5+    , Generic1 -- ^ @since 0.5+    )++-- not provided because it clashes with GHC.TypeLits.^+-- infixr 8 ^+-- The exclusive disjunction of two predicates.+-- type (^) = Xor++-- | @since 0.5+instance ( Predicate l x, Predicate r x, Typeable l, Typeable r+         ) => Predicate (Xor l r) x where+  validate p x = do+    let left = validate @l undefined x+    let right = validate @r undefined x+    case (left, right) of+      (Nothing, Nothing) -> Just (RefineXorException (typeOf p) Nothing)+      (Just  l, Just  r) -> Just (RefineXorException (typeOf p) (Just (l, r)))+      _ -> Nothing++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value has a length+-- which is less than the specified type-level number.+--+--   >>> isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])+--   True+--+--   >>> isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])+--   True+--+--   >>> isRight (refine @(SizeLessThan 4) @Text "Hi")+--   True+--+--   >>> isLeft (refine @(SizeLessThan 4) @Text "Hello")+--   True+--+--   @since 0.2.0.0+data SizeLessThan (n :: Nat)+  = SizeLessThan -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.2.0.0+instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where+  validate p x = sized p (x, "Foldable") length ((<), "less than")+-- | @since 0.5+instance (KnownNat n) => Predicate (SizeLessThan n) Text where+  validate p x = sized p (x, "Text") Text.length ((<), "less than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeLessThan n) BS.ByteString where+  validate p x = sized p (x, "ByteString") BS.length ((<), "less than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeLessThan n) BL.ByteString where+  validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((<), "less than")++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value has a length+-- which is greater than the specified type-level number.+--+--   >>> isLeft (refine  @(SizeGreaterThan 3) @[Int] [1,2,3])+--   True+--+--   >>> isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])+--   True+--+--   >>> isLeft (refine @(SizeGreaterThan 4) @Text "Hi")+--   True+--+--   >>> isRight (refine @(SizeGreaterThan 4) @Text "Hello")+--   True+--+--   @since 0.2.0.0+data SizeGreaterThan (n :: Nat)+  = SizeGreaterThan -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.2.0.0+instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where+  validate p x = sized p (x, "Foldable") length ((>), "greater than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeGreaterThan n) Text where+  validate p x = sized p (x, "Text") Text.length ((>), "greater than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeGreaterThan n) BS.ByteString where+  validate p x = sized p (x, "ByteString") BS.length ((>), "greater than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeGreaterThan n) BL.ByteString where+  validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((>), "greater than")++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value has a length+-- which is equal to the specified type-level number.+--+--   >>> isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])+--   True+--+--   >>> isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])+--   True+--+--   >>> isRight (refine @(SizeEqualTo 4) @Text "four")+--   True+--+--   >>> isLeft (refine @(SizeEqualTo 35) @Text "four")+--   True+--+--   @since 0.2.0.0+data SizeEqualTo (n :: Nat)+  = SizeEqualTo -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.2.0.0+instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where+  validate p x = sized p (x, "Foldable") length ((==), "equal to")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeEqualTo n) Text where+  validate p x = sized p (x, "Text") Text.length ((==), "equal to")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeEqualTo n) BS.ByteString where+  validate p x = sized p (x, "ByteString") BS.length ((==), "equal to")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeEqualTo n) BL.ByteString where+  validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((==), "equal to")++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the 'Foldable' contains elements+-- in a strictly ascending order.+--+--   >>> isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])+--   True+--+--   >>> isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])+--   True+--+--   @since 0.2.0.0+data Ascending+  = Ascending -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.2.0.0+instance (Foldable t, Ord a) => Predicate Ascending (t a) where+  validate p x = do+    if increasing x+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         "Foldable is not in ascending order."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the 'Foldable' contains elements+-- in a strictly descending order.+--+--   >>> isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])+--   True+--+--   >>> isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])+--   True+--+--   @since 0.2.0.0+data Descending+  = Descending -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.2.0.0+instance (Foldable t, Ord a) => Predicate Descending (t a) where+  validate p x = do+    if decreasing x+    then Nothing+    else throwRefineOtherException+        (typeOf p)+        "Foldable is not in descending order."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is less than the+--   specified type-level number.+--+--   >>> isRight (refine @(LessThan 12) @Int 11)+--   True+--+--   >>> isLeft (refine @(LessThan 12) @Int 12)+--   True+--+--   @since 0.1.0.0+data LessThan (n :: Nat)+  = LessThan -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.1.0.0+instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where+  validate p x = do+    let x' = fromIntegral (natVal p)+    if x < x'+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         ("Value is not less than " <> PP.pretty (natVal p))++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is greater than the+--   specified type-level number.+--+--   >>> isRight (refine @(GreaterThan 65) @Int 67)+--   True+--+--   >>> isLeft (refine @(GreaterThan 65) @Int 65)+--   True+--+--   @since 0.1.0.0+data GreaterThan (n :: Nat)+  = GreaterThan -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.1.0.0+instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where+  validate p x = do+    let x' = fromIntegral (natVal p)+    if x > x'+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         ("Value is not greater than " <> PP.pretty (natVal p))++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is greater than or equal to the+--   specified type-level number.+--+--   >>> isRight (refine @(From 9) @Int 10)+--   True+--+--   >>> isRight (refine @(From 10) @Int 10)+--   True+--+--   >>> isLeft (refine @(From 11) @Int 10)+--   True+--+--   @since 0.1.2+data From (n :: Nat)+  = From -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.1.2+instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where+  validate p x = do+    let x' = fromIntegral (natVal p)+    if x >= x'+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         ("Value is less than " <> PP.pretty (natVal p))++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is less than or equal to the+--   specified type-level number.+--+--   >>> isRight (refine @(To 23) @Int 17)+--   True+--+--   >>> isLeft (refine @(To 17) @Int 23)+--   True+--+--   @since 0.1.2+data To (n :: Nat)+  = To -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.1.2+instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where+  validate p x = do+    let x' = fromIntegral (natVal p)+    if x <= x'+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         ("Value is greater than " <> PP.pretty (natVal p))++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is within an inclusive range.+--+--   >>> isRight (refine @(FromTo 0 16) @Int 13)+--   True+--+--   >>> isRight (refine @(FromTo 13 15) @Int 13)+--   True+--+--   >>> isRight (refine @(FromTo 13 15) @Int 15)+--   True+--+--   >>> isLeft (refine @(FromTo 13 15) @Int 12)+--   True+--+--   @since 0.1.2+data FromTo (mn :: Nat) (mx :: Nat)+  = FromTo -- ^ @since 0.4.2+  deriving+    ( Generic-- ^ @since 0.3.0.0+    )++-- | @since 0.1.2+instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx+         ) => Predicate (FromTo mn mx) x where+  validate p x = do+    let mn' = natVal (Proxy @mn)+    let mx' = natVal (Proxy @mx)+    if x >= fromIntegral mn' && x <= fromIntegral mx'+    then Nothing+    else+      let msg = [ "Value is out of range (minimum: "+                , PP.pretty mn'+                , ", maximum: "+                , PP.pretty mx'+                , ")"+                ] |> mconcat+      in throwRefineOtherException (typeOf p) msg++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is equal to the specified+--   type-level number @n@.+--+--   >>> isRight (refine @(EqualTo 5) @Int 5)+--   True+--+--   >>> isLeft (refine @(EqualTo 6) @Int 5)+--   True+--+--   @since 0.1.0.0+data EqualTo (n :: Nat)+  = EqualTo -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.1.0.0+instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where+  validate p x = do+    let x' = fromIntegral (natVal p)+    if x == x'+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         ("Value does not equal " <> PP.pretty (natVal p))++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is not equal to the specified+--   type-level number @n@.+--+--   >>> isRight (refine @(NotEqualTo 6) @Int 5)+--   True+--+--   >>> isLeft (refine @(NotEqualTo 5) @Int 5)+--   True+--+--   @since 0.2.0.0+data NotEqualTo (n :: Nat)+  = NotEqualTo -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.2.0.0+instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where+  validate p x = do+    let x' = fromIntegral (natVal p)+    if x /= x'+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         ("Value does equal " <> PP.pretty (natVal p))++--------------------------------------------------------------------------------++-- | 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@.+--+--   >>> isRight (refine @(NegativeFromTo 5 12) @Int (-3))+--   True+--+--   >>> isLeft (refine @(NegativeFromTo 4 3) @Int (-5))+--   True+--+--   @since 0.4+data NegativeFromTo (n :: Nat) (m :: Nat)+  = NegativeFromTo -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.4+instance (Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m) x where+  validate p x = do+    let n' = natVal (Proxy @n)+    let m' = natVal (Proxy @m)+    if x >= fromIntegral (negate n') && x <= fromIntegral m'+    then Nothing+    else+      let msg = [ "Value is out of range (minimum: "+                , PP.pretty (negate n')+                , ", maximum: "+                , PP.pretty m'+                , ")"+                ] |> mconcat+      in throwRefineOtherException (typeOf p) msg++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is divisible by @n@.+--+--   >>> isRight (refine @(DivisibleBy 3) @Int 12)+--   True+--+--   >>> isLeft (refine @(DivisibleBy 2) @Int 37)+--   True+--+--   @since 0.4.2+data DivisibleBy (n :: Nat)+  = DivisibleBy -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.4.2+instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where+  validate p x = do+    let x' = fromIntegral (natVal p)+    if x `mod` x' == 0+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         ("Value is not divisible by " <> PP.pretty (natVal p))++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is odd.+--+--   >>> isRight (refine @Odd @Int 33)+--   True+--+--   >>> isLeft (refine @Odd @Int 32)+--   True+--+--   @since 0.4.2+data Odd+  = Odd -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | @since 0.4.2+instance (Integral x) => Predicate Odd x where+  validate p x = do+    if odd x+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         "Value is not odd."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is IEEE "not-a-number" (NaN).+--+--   >>> isRight (refine @NaN @Double (0/0))+--   True+--+--   >>> isLeft (refine @NaN @Double 13.9)+--   True+--+--   @since 0.5+data NaN+  = NaN -- ^ @since 0.5+  deriving+    ( Generic -- ^ @since 0.5+    )++-- | @since 0.5+instance (RealFloat x) => Predicate NaN x where+  validate p x = do+    if isNaN x+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         "Value is not IEEE \"not-a-number\" (NaN)."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is IEEE infinity or negative infinity.+--+--   >>> isRight (refine @Infinite @Double (1/0))+--   True+--+--   >>> isRight (refine @Infinite @Double (-1/0))+--   True+--+--   >>> isLeft (refine @Infinite @Double 13.20)+--   True+--+--   @since 0.5+data Infinite+  = Infinite -- ^ @since 0.5+  deriving+    ( Generic -- ^ @since 0.5+    )++-- | @since 0.5+instance (RealFloat x) => Predicate Infinite x where+  validate p x = do+    if isInfinite x+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         "Value is not IEEE infinity or negative infinity."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is even.+--+--   >>> isRight (refine @Even @Int 32)+--   True+--+--   >>> isLeft (refine @Even @Int 33)+--   True+--+--   @since 0.4.2+data Even+  = Even -- ^ @since 0.4.2+  deriving+    ( Generic -- ^ @since 0.4.2+    )++-- | @since 0.4.2+instance (Integral x) => Predicate Even x where+  validate p x = do+    if even x+    then Nothing+    else throwRefineOtherException+         (typeOf p)+         "Value is not even."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is greater than zero.+--+--   @since 0.1.0.0+type Positive = GreaterThan 0++-- | A 'Predicate' ensuring that the value is less than or equal to zero.+--+--   @since 0.1.2+type NonPositive = To 0++-- | A 'Predicate' ensuring that the value is less than zero.+--+--   @since 0.1.0.0+type Negative = LessThan 0++-- | A 'Predicate' ensuring that the value is greater than or equal to zero.+--+--   @since 0.1.2+type NonNegative = From 0++-- | An inclusive range of values from zero to one.+--+--   @since 0.1.0.0+type ZeroToOne = FromTo 0 1++-- | A 'Predicate' ensuring that the value is not equal to zero.+--+--   @since 0.2.0.0+type NonZero = NotEqualTo 0++-- | A 'Predicate' ensuring that the type is non-empty.+--+--   @since 0.5+type Empty = SizeEqualTo 0++-- | A 'Predicate' ensuring that the type is non-empty.+--+--   @since 0.2.0.0+type NonEmpty = SizeGreaterThan 0++--------------------------------------------------------------------------------++-- | A typeclass containing "safe" conversions between refined+--   predicates where the target is /weaker/ than the source:+--   that is, all values that satisfy the first predicate will+--   be guaranteed to satisy the second.+--+--   Take care: writing an instance declaration for your custom+--   predicates is the same as an assertion that 'weaken' is+--   safe to use:+--+--   @+--   instance 'Weaken' Pred1 Pred2+--   @+--+--   For most of the instances, explicit type annotations for+--   the result value's type might be required.+--+-- @since 0.2.0.0+class Weaken from to where+  -- | @since 0.2.0.0+  weaken :: Refined from x -> Refined to x+  weaken = coerce++-- | @since 0.2.0.0+instance (n <= m)         => Weaken (LessThan n)    (LessThan m)+-- | @since 0.2.0.0+instance (n <= m)         => Weaken (LessThan n)    (To m)+-- | @since 0.2.0.0+instance (n <= m)         => Weaken (To n)          (To m)+-- | @since 0.2.0.0+instance (m <= n)         => Weaken (GreaterThan n) (GreaterThan m)+-- | @since 0.2.0.0+instance (m <= n)         => Weaken (GreaterThan n) (From m)+-- | @since 0.2.0.0+instance (m <= n)         => Weaken (From n)        (From m)+-- | @since 0.2.0.0+instance (p <= n, m <= q) => Weaken (FromTo n m)    (FromTo p q)+-- | @since 0.2.0.0+instance (p <= n)         => Weaken (FromTo n m)    (From p)+-- | @since 0.2.0.0+instance (m <= q)         => Weaken (FromTo n m)    (To q)++-- | This function helps type inference.+--   It is equivalent to the following:+--+-- @+-- instance Weaken (And l r) l+-- @+--+--   @since 0.2.0.0+andLeft :: Refined (And l r) x -> Refined l x+andLeft = coerce++-- | This function helps type inference.+--   It is equivalent to the following:+--+-- @+-- instance Weaken (And l r) r+-- @+--+--   @since 0.2.0.0+andRight :: Refined (And l r) x -> Refined r x+andRight = coerce++-- | This function helps type inference.+--   It is equivalent to the following:+--+-- @+-- instance Weaken l (Or l r)+-- @+--+--   @since 0.2.0.0+leftOr :: Refined l x -> Refined (Or l r) x+leftOr = coerce++-- | This function helps type inference.+--   It is equivalent to the following:+--+-- @+-- instance Weaken r (Or l r)+-- @+--+--   @since 0.2.0.0+rightOr :: Refined r x -> Refined (Or l r) x+rightOr = coerce++-- | Strengthen a refinement by composing it with another.+--+--   @since 0.4.2.2+strengthen :: forall p p' x. (Predicate p x, Predicate p' x)+  => Refined p x+  -> Either RefineException (Refined (p && p') x)+strengthen r = refine @(p && p') (unrefine r)+{-# inlineable strengthen #-}++--------------------------------------------------------------------------------++-- | An exception encoding the way in which a 'Predicate' failed.+--+--   @since 0.2.0.0+data RefineException+  = -- | A 'RefineException' for failures involving the 'Not' predicate.+    --+    --   @since 0.2.0.0+    RefineNotException+    { _RefineException_typeRep   :: !TypeRep+      -- ^ The 'TypeRep' of the @'Not' p@ type.+    }++  | -- | A 'RefineException' for failures involving the 'And' predicate.+    --+    --   @since 0.2.0.0+    RefineAndException+    { _RefineException_typeRep   :: !TypeRep+      -- ^ The 'TypeRep' of the @'And' l r@ type.+    , _RefineException_andChild  :: !(These RefineException RefineException)+      -- ^ A 'These' encoding which branch(es) of the 'And' failed:+      --   if the 'RefineException' came from the @l@ predicate, then+      --   this will be 'This', if it came from the @r@ predicate, this+      --   will be 'That', and if it came from both @l@ and @r@, this+      --   will be 'These'.++      -- note to self: what am I, Dr. Seuss?+    }++  | -- | A 'RefineException' for failures involving the 'Or' predicate.+    --+    --   @since 0.2.0.0+    RefineOrException+    { _RefineException_typeRep   :: !TypeRep+      -- ^ The 'TypeRep' of the @'Or' l r@ type.+    , _RefineException_orLChild  :: !RefineException+      -- ^ The 'RefineException' for the @l@ failure.+    , _RefineException_orRChild  :: !RefineException+      -- ^ The 'RefineException' for the @l@ failure.+    }++  | -- | A 'RefineException' for failures involving the 'Xor' predicate.+    --+    --   @since 0.5+    RefineXorException+    { _RefineException_typeRep   :: !TypeRep+    , _RefineException_children  :: !(Maybe (RefineException, RefineException))+    }++  | -- | A 'RefineException' for failures involving all other predicates.+    --+    --   @since 0.2.0.0+    RefineOtherException+    { _RefineException_typeRep   :: !TypeRep+      -- ^ The 'TypeRep' of the predicate that failed.+    , _RefineException_message   :: !(PP.Doc Void)+      -- ^ A custom message to display.+    }+  | -- | A 'RefineException' for failures involving all other predicates with custom exception.+    --+    --   @since 0.5+    RefineSomeException+    { _RefineException_typeRep   :: !TypeRep+      -- ^ The 'TypeRep' of the predicate that failed.+    , _RefineException_Exception :: !SomeException+      -- ^ A custom exception.+    }+  deriving+    ( Generic -- ^ @since 0.3.0.0+    )++-- | /Note/: Equivalent to @'displayRefineException'@.+--+--   @since 0.2.0.0+instance Show RefineException where+  show = PP.pretty .> show++data ExceptionTree a+  = NodeNone+  | NodeSome !TypeRep SomeException+  | NodeOther !TypeRep !(PP.Doc Void)+  | NodeNot !TypeRep+  | NodeOr !TypeRep [ExceptionTree a]+  | NodeAnd !TypeRep [ExceptionTree a]+  | NodeXor !TypeRep [ExceptionTree a]++showTree :: ExceptionTree RefineException -> PP.Doc ann+showTree = PP.pretty . unlines . showOne "  " "" ""+  where+    showOne :: String -> String -> String -> ExceptionTree RefineException -> [String]+    showOne leader tie arm = \case+      NodeNone ->+        [+        ]+      NodeSome tr e ->+        [ leader+          <> arm+          <> tie+          <> "The predicate ("+          <> show tr+          <> ") failed with the exception: "+          <> displayException e+          <> "."+        ]+      NodeOther tr p ->+        [ leader+          <> arm+          <> tie+          <> "The predicate ("+          <> show tr+          <> ") failed with the message: "+          <> show p+          <> "."+        ]+      NodeNot tr ->+        [ leader+          <> arm+          <> tie+          <> "The predicate ("+          <> show tr+          <> ") does not hold."+        ]+      NodeOr tr rest -> nodeRep tr : showChildren rest (leader <> extension)+      NodeAnd tr rest -> nodeRep tr : showChildren rest (leader <> extension)+      -- can be empty since both can be satisfied+      NodeXor tr [] ->+        [ leader+          <> arm+          <> tie+          <> "The predicate ("+          <> show tr+          <> ") does not hold, because both predicates were satisfied."+        ]+      NodeXor tr rest -> nodeRep tr : showChildren rest (leader <> extension)+      where+        nodeRep :: TypeRep -> String+        -- TODO: make tr bold+        nodeRep tr = leader <> arm <> tie <> show tr++        extension :: String+        extension = case arm of+          ""  -> ""+          "└" -> "    "+          _   -> "│   "++    showChildren :: [ExceptionTree RefineException] -> String -> [String]+    showChildren children leader =+      let arms = replicate (length children - 1) "├" <> ["└"]+      in concat (zipWith (showOne leader "── ") arms children)++refineExceptionToTree :: RefineException -> ExceptionTree RefineException+refineExceptionToTree = go+  where+    go = \case+      RefineSomeException tr e -> NodeSome tr e+      RefineOtherException tr p -> NodeOther tr p+      RefineNotException tr -> NodeNot tr+      RefineOrException tr l r -> NodeOr tr [go l, go r]+      RefineAndException tr (This l) -> NodeAnd tr [go l]+      RefineAndException tr (That r) -> NodeAnd tr [go r]+      RefineAndException tr (These l r) -> NodeAnd tr [go l, go r]+      RefineXorException tr Nothing -> NodeXor tr []+      RefineXorException tr (Just (l, r)) -> NodeXor tr [go l, go r]++-- | Display a 'RefineException' as a @'PP.Doc' ann@+--+--   This function can be extremely useful for debugging+--   @'RefineException's@, especially deeply nested ones.+--+--   Consider:+--+--   @+--   myRefinement = refine+--     \@(And+--         (Not (LessThan 5))+--         (Xor+--           (DivisibleBy 10)+--           (And+--             (EqualTo 4)+--             (EqualTo 3)+--           )+--         )+--      )+--     \@Int+--     3+--   @+--+--   This function will show the following tree structure, recursively breaking down+--   every issue:+--+--   @+--   And (Not (LessThan 5)) (Xor (EqualTo 4) (And (EqualTo 4) (EqualTo 3)))+--   ├── The predicate (Not (LessThan 5)) does not hold.+--   └── Xor (DivisibleBy 10) (And (EqualTo 4) (EqualTo 3))+--       ├── The predicate (DivisibleBy 10) failed with the message: Value is not divisible by 10+--       └── And (EqualTo 4) (EqualTo 3)+--           └── The predicate (EqualTo 4) failed with the message: Value does not equal 4+--   @+--+--   /Note/: Equivalent to @'show' \@'RefineException'@+--+--   @since 0.2.0.0+displayRefineException :: RefineException -> PP.Doc ann+displayRefineException = refineExceptionToTree .> showTree++-- | Pretty-print a 'RefineException'.+--+--   /Note/: Equivalent to 'displayRefineException'.+--+--   @since 0.2.0.0+instance PP.Pretty RefineException where+  pretty = displayRefineException++-- | Encode a 'RefineException' for use with \Control.Exception\.+--+--   /Note/: Equivalent to @'displayRefineException'@.+--+--   @since 0.2.0.0+instance Exception RefineException where+  displayException = show++--------------------------------------------------------------------------------++-- | A handler for a @'RefineException'@.+--+--   'throwRefineOtherException' is useful for defining what+--   behaviour 'validate' should have in the event of a predicate failure.+--+--   @since 0.2.0.0+throwRefineOtherException+  :: TypeRep+  -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'.+  -> PP.Doc Void+  -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed.+  -> Maybe RefineException+throwRefineOtherException rep+  = RefineOtherException rep .> Just++-- | A handler for a @'RefineException'@.+--+--   'throwRefineSomeException' is useful for defining what+--   behaviour 'validate' should have in the event of a predicate failure+--   with a specific exception.+--+--   @since 0.5+throwRefineSomeException+  :: TypeRep+  -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'.+  -> SomeException+  -- ^ A custom exception.+  -> Maybe RefineException+throwRefineSomeException rep+  = RefineSomeException rep .> Just++-- | An implementation of 'validate' that always succeeds.+--+--   ==== __Examples__+--+--   @+--   data ContainsLetterE = ContainsLetterE+--+--   instance Predicate ContainsLetterE 'Text' where+--     validate _ t = do+--       if 'Data.Text.any' ('==' \'e\') t+--       then 'Nothing'+--       else 'success'+--   @+--+--   @since 0.5+success+  :: Maybe RefineException+success+  = Nothing++--------------------------------------------------------------------------------++-- | Helper function for sized predicates.+sized :: (Typeable (p n), KnownNat n)+  => p n+     -- ^ predicate+  -> (a, PP.Doc Void)+     -- ^ (value, type)+  -> (a -> Int)+     -- ^ length of value+  -> (Int -> Int -> Bool, PP.Doc Void)+     -- ^ (compare :: Length -> KnownNat -> Bool, comparison string)+  -> Maybe RefineException+sized p (x, typ) lenF (cmp, cmpDesc) = do+  let x' = fromIntegral (natVal p)+  let sz = lenF x+  if cmp sz x'+  then Nothing+  else+    let msg =+          [ "Size of ", typ, " is not ", cmpDesc+          , PP.pretty x'+          , "\n  "+          , "Size is: "+          , PP.pretty sz+          ] |> mconcat+    in throwRefineOtherException (typeOf p) msg

@@ -1,1150 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai------ 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                        #-}-{-# OPTIONS_GHC -funbox-strict-fields        #-}------------------------------------------------------------------------------------{-# LANGUAGE AllowAmbiguousTypes        #-}-{-# 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                #-}-{-# LANGUAGE RankNTypes                 #-}-{-# LANGUAGE RoleAnnotations            #-}-{-# LANGUAGE ScopedTypeVariables        #-}-{-# LANGUAGE TemplateHaskell            #-}-{-# LANGUAGE TypeApplications           #-}-{-# LANGUAGE TypeFamilies               #-}-{-# LANGUAGE TypeOperators              #-}-{-# LANGUAGE UndecidableInstances       #-}-------------------------------------------------------------------------------------- | In type theory, a refinement type is a type endowed---   with a predicate which is assumed to hold for any element---   of the refined type.------   This library allows one to capture the idea of a refinement type---   using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value---   of type @x@, ensuring that it satisfies a type-level predicate @p@.------   A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/----module Refined.Internal-  ( -- * 'Refined'-    Refined(Refined)--    -- ** Creation-  , refine-  , refine_-  , refineThrow-  , refineFail-  , refineError-  , refineTH-  , refineTH_--    -- ** Consumption-  , unrefine--    -- * 'Predicate'-  , Predicate (validate)-  , reifyPredicate--    -- * Logical predicates-  , Not(..)-  , And(..)-  , type (&&)-  , Or(..)-  , type (||)--    -- * Identity predicate-  , IdPred(..)--    -- * Numeric predicates-  , LessThan(..)-  , GreaterThan(..)-  , From(..)-  , To(..)-  , FromTo(..)-  , NegativeFromTo(..)-  , EqualTo(..)-  , NotEqualTo(..)-  , Odd(..)-  , Even(..)-  , DivisibleBy(..)-  , Positive-  , NonPositive-  , Negative-  , NonNegative-  , ZeroToOne-  , NonZero--    -- * Foldable predicates-  , SizeLessThan(..)-  , SizeGreaterThan(..)-  , SizeEqualTo(..)-  , NonEmpty--    -- * IsList predicates-  , Ascending(..)-  , Descending(..)--    -- * Weakening-  , Weaken (weaken)-  , andLeft-  , andRight-  , leftOr-  , rightOr--    -- * Strengthening-  , strengthen-  , strengthenM--    -- * Error handling--    -- ** 'RefineException'-  , RefineException-    ( RefineNotException-    , RefineAndException-    , RefineOrException-    , RefineOtherException-    )-  , displayRefineException--    -- ** 'RefineT' and 'RefineM'-  , RefineT, runRefineT, exceptRefine, mapRefineT-  , RefineM, refineM, runRefineM-  , throwRefine, catchRefine-  , throwRefineOtherException--  , (|>)-  , (.>)--    -- * Re-Exports-  , PP.pretty- ) where------------------------------------------------------------------------------------import           Prelude-                 (Num, fromIntegral, negate, undefined)--import           Control.Applicative          (Applicative (pure))-import           Control.Exception            (Exception (displayException))-import           Control.Monad                (Monad, unless, when)-import           Data.Bool                    (Bool(True,False),(&&), otherwise)-import           Data.Coerce                  (coerce)-import           Data.Either-                 (Either (Left, Right), either, isRight)-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.Monoid                  (mconcat)-import           Data.Ord                     (Ord, (<), (<=), (>), (>=))-import           Data.Proxy                   (Proxy (Proxy))-import           Data.Semigroup               (Semigroup((<>)))-import           Data.Typeable                (TypeRep, Typeable, typeOf)-import           Data.Void                    (Void)-import           Text.Read                    (Read (readsPrec), lex, readParen)-import           Text.Show                    (Show (show))--import           Control.Monad.Catch          (MonadThrow)-import qualified Control.Monad.Catch          as MonadThrow-import           Control.Monad.Error.Class    (MonadError)-import qualified Control.Monad.Error.Class    as MonadError-import           Control.Monad.Fail           (MonadFail, fail)-import           Control.Monad.Fix            (MonadFix, fix)-import           Control.Monad.Trans.Class    (MonadTrans (lift))--import           Control.Monad.Trans.Except   (ExceptT)-import qualified Control.Monad.Trans.Except   as ExceptT--import           GHC.Generics                 (Generic, Generic1)-import           GHC.TypeLits                 (type (<=), KnownNat, Nat, natVal)--import           GHC.Real                     (Integral(mod), even, odd)--import           Refined.These                (These(This,That,These))--import qualified Data.Text.Prettyprint.Doc    as PP-import qualified Language.Haskell.TH.Syntax   as TH-------------------------------------------------------------------------------------- $setup------ Doctest imports------ >>> :set -XDataKinds--- >>> :set -XTypeApplications--- >>> import Data.Int--- >>> import Data.Either (isLeft)---------------------------------------------------------------------------------------infixl 0 |>-infixl 9 .>---- | Helper function, stolen from the 'flow' package.-(|>) :: a -> (a -> b) -> b-(|>) = flip ($)-{-# INLINE (|>) #-}---- | Helper function, stolen from the 'flow' package.-(.>) :: (a -> b) -> (b -> c) -> a -> c-f .> g = \x -> g (f x)-{-# INLINE (.>) #-}---- | FIXME: doc-data Ordered a = Empty | Decreasing a | Increasing a---- | FIXME: doc-inc :: Ordered a -> Bool-inc (Decreasing _) = False-inc _              = True-{-# INLINE inc #-}---- | FIXME: doc-dec :: Ordered a -> Bool-dec (Increasing _) = False-dec _              = True-{-# INLINE dec #-}--increasing :: (Foldable t, Ord a) => t a -> Bool-increasing = inc . foldl' go Empty where-  go Empty y = Increasing y-  go (Decreasing x) _ = Decreasing x-  go (Increasing x) y-    | x <= y = Increasing y-    | otherwise = Decreasing y-{-# INLINABLE increasing #-}--decreasing :: (Foldable t, Ord a) => t a -> Bool-decreasing = dec . foldl' go Empty where-  go Empty y = Decreasing y-  go (Increasing x) _ = Increasing x-  go (Decreasing x) y-    | x >= y = Decreasing y-    | otherwise = Increasing y-{-# INLINABLE decreasing #-}-------------------------------------------------------------------------------------- | A refinement type, which wraps a value of type @x@,---   ensuring that it satisfies a type-level predicate @p@.-newtype Refined p x = Refined x-  deriving (Eq, Foldable , Ord, Show, Typeable)--type role Refined nominal nominal---- | This instance makes sure to check the refinement.-instance (Read x, Predicate p x) => Read (Refined p x) where-  readsPrec d = readParen (d > 10) $ \r1 -> do-    ("Refined", r2) <- lex r1-    (raw,       r3) <- readsPrec 11 r2-    case refine raw of-      Right val -> [(val, r3)]-      Left  _   -> []--instance (TH.Lift x) => TH.Lift (Refined p x) where-  lift (Refined a) = [|Refined a|]-------------------------------------------------------------------------------------- | A smart constructor of a 'Refined' value.---   Checks the input value at runtime.-refine :: (Predicate p x) => x -> Either RefineException (Refined p x)-refine x = do-  let predicateByResult :: RefineM (Refined p x) -> p-      predicateByResult = const undefined-  runRefineM $ fix $ \result -> do-    validate (predicateByResult result) x-    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.-refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)-refineThrow = refine .> either MonadThrow.throwM pure-{-# INLINABLE refineThrow #-}---- | Constructs a 'Refined' value at run-time,---   calling 'Control.Monad.Fail.fail' if the value---   does not satisfy the predicate.-refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)-refineFail = refine .> either (displayException .> fail) pure-{-# INLINABLE refineFail #-}---- | Constructs a 'Refined' value at run-time,---   calling 'Control.Monad.Error.throwError' if the value---   does not satisfy the predicate.-refineError :: (Predicate p x, MonadError RefineException m)-            => x -> m (Refined p x)-refineError = refine .> either MonadError.throwError pure-{-# INLINABLE refineError #-}-------------------------------------------------------------------------------------- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@.------   For example:------   > $$(refineTH 23) :: Refined Positive Int---   > Refined 23------   Here's an example of an invalid value:------   > $$(refineTH 0) :: Refined Positive Int---   > <interactive>:6:4:---   >     Value is not greater than 0---   >     In the Template Haskell splice $$(refineTH 0)---   >     In the expression: $$(refineTH 0) :: Refined Positive Int---   >     In an equation for ‘it’:---   >         it = $$(refineTH 0) :: Refined Positive Int------   If it's not evident, the example above indicates a compile-time failure,---   which means that the checking was done at compile-time, thus introducing a---   zero runtime overhead compared to a plain value construction.------   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---- | 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.-{-# INLINE unrefine #-}-unrefine :: Refined p x -> x-unrefine = coerce-------------------------------------------------------------------------------------- | A typeclass which defines a runtime interpretation of---   a type-level predicate @p@ for type @x@.-class (Typeable p) => Predicate p x where-  {-# MINIMAL validate #-}-  -- | Check the value @x@ according to the predicate @p@,-  --   producing an error string if the value does not satisfy.-  validate :: (Monad m) => p -> x -> RefineT m ()-------------------------------------------------------------------------------------- | Reify a 'Predicate' by turning it into a value-level predicate.-reifyPredicate :: forall p a. Predicate p a => a -> Bool-reifyPredicate = refine @p @a .> isRight-------------------------------------------------------------------------------------- | A predicate which is satisfied for all types.---   Arguments passed to @'validate'@ in @'validate' 'IdPred' x@---   are not evaluated.------   >>> isRight (refine @IdPred @Int undefined)---   True------   >>> isLeft (refine @IdPred @Int undefined)---   False----data IdPred = IdPred-  deriving (Generic)--instance Predicate IdPred x where-  validate _ _ = pure ()-  {-# INLINE validate #-}-------------------------------------------------------------------------------------- | The negation of a predicate.------   >>> isRight (refine @(Not NonEmpty) @[Int] [])---   True------   >>> isLeft (refine @(Not NonEmpty) @[Int] [1,2])---   True-data Not p = Not-  deriving (Generic, Generic1)--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))-------------------------------------------------------------------------------------- | The conjunction of two predicates.------   >>> isLeft (refine @(And Positive Negative) @Int 3)---   True------   >>> isRight (refine @(And Positive Odd) @Int 203)---   True-data And l r = And-  deriving (Generic, Generic1)--infixr 3 &&--- | The conjunction of two predicates.-type (&&) = And--instance ( Predicate l x, Predicate r x, Typeable l, Typeable r-         ) => Predicate (And l r) x where-  validate p x = do-    a <- lift $ runRefineT $ validate @l undefined x-    b <- lift $ runRefineT $ validate @r undefined x-    let throw err = throwRefine (RefineAndException (typeOf p) err)-    case (a, b) of-      (Left  e, Left e1) -> throw (These e e1)-      (Left  e,       _) -> throw (This e)-      (Right _, Left  e) -> throw (That e)-      (Right _, Right _) -> pure ()-------------------------------------------------------------------------------------- | The disjunction of two predicates.------   >>> isRight (refine @(Or Even Odd) @Int 3)---   True------   >>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)---   True-data Or l r = Or-  deriving (Generic, Generic1)--infixr 2 ||--- | The disjunction of two predicates.-type (||) = Or--instance ( Predicate l x, Predicate r x, Typeable l, Typeable r-         ) => Predicate (Or l r) x where-  validate p x = do-    left  <- lift $ runRefineT $ validate @l undefined x-    right <- lift $ runRefineT $ validate @r undefined x-    case (left, right) of-      (Left l, Left r) -> throwRefine (RefineOrException (typeOf p) l r)-      _                -> pure ()-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' has a length--- which is less than the specified type-level number.------   >>> isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])---   True------   >>> isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])---   True-data SizeLessThan (n :: Nat) = SizeLessThan-  deriving (Generic)--instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where-  validate p x = do-    let x' = natVal p-        sz = length x-    unless (sz < fromIntegral x') $ do-      throwRefineOtherException (typeOf p)-        ( [ "Size of Foldable is not less than "-          , PP.pretty x'-          , newline-          , twoSpaces-          , "Size is: "-          , PP.pretty sz-          ] |> mconcat-        )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' has a length--- which is greater than the specified type-level number.------   >>> isLeft (refine  @(SizeGreaterThan 3) @[Int] [1,2,3])---   True------   >>> isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])---   True--data SizeGreaterThan (n :: Nat) = SizeGreaterThan-  deriving (Generic)--instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where-  validate p x = do-    let x' = natVal p-        sz = length x-    unless (sz > fromIntegral x') $ do-      throwRefineOtherException (typeOf p)-        ( [ "Size of Foldable is not greater than "-          , PP.pretty x'-          , newline-          , twoSpaces-          , "Size is: "-          , PP.pretty sz-          ] |> mconcat-        )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' has a length--- which is equal to the specified type-level number.------   >>> isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])---   True------   >>> isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])---   True-data SizeEqualTo (n :: Nat) = SizeEqualTo-  deriving (Generic)--instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where-  validate p x = do-    let x' = natVal p-        sz = length x-    unless (sz == fromIntegral x') $ do-      throwRefineOtherException (typeOf p)-        ( [ "Size of Foldable is not equal to "-          , PP.pretty x'-          , newline-          , twoSpaces-          , "Size is: "-          , PP.pretty sz-          ] |> mconcat-        )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' contains elements--- in a strictly ascending order.------   >>> isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])---   True------   >>> isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])---   True-data Ascending = Ascending-  deriving (Generic)--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." )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' contains elements--- in a strictly descending order.------   >>> isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])---   True------   >>> isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])---   True-data Descending = Descending-  deriving (Generic)--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." )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is less than the---   specified type-level number.------   >>> isRight (refine @(LessThan 12) @Int 11)---   True------   >>> isLeft (refine @(LessThan 12) @Int 12)---   True-data LessThan (n :: Nat) = LessThan-  deriving (Generic)--instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where-  validate p x = do-    let x' = natVal p-    unless (x < fromIntegral x') $ do-      throwRefineOtherException (typeOf p) ( "Value is not less than " <> PP.pretty x' )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is greater than the---   specified type-level number.------   >>> isRight (refine @(GreaterThan 65) @Int 67)---   True------   >>> isLeft (refine @(GreaterThan 65) @Int 65)---   True-data GreaterThan (n :: Nat) = GreaterThan-  deriving (Generic)--instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where-  validate p x = do-    let x' = natVal p-    unless (x > fromIntegral x') $ do-      throwRefineOtherException (typeOf p) ( "Value is not greater than " <> PP.pretty x' )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is greater than or equal to the---   specified type-level number.------   >>> isRight (refine @(From 9) @Int 10)---   True------   >>> isRight (refine @(From 10) @Int 10)---   True------   >>> isLeft (refine @(From 11) @Int 10)---   True-data From (n :: Nat) = From-  deriving (Generic)--instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where-  validate p x = do-    let x' = natVal p-    unless (x >= fromIntegral x') $ do-      throwRefineOtherException (typeOf p) ( "Value is less than " <> PP.pretty x' )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is less than or equal to the---   specified type-level number.------   >>> isRight (refine @(To 23) @Int 17)---   True------   >>> isLeft (refine @(To 17) @Int 23)---   True-data To (n :: Nat) = To-  deriving (Generic)--instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where-  validate p x = do-    let x' = natVal p-    unless (x <= fromIntegral x') $ do-      throwRefineOtherException (typeOf p) ( "Value is greater than " <> PP.pretty x' )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is within an inclusive range.------   >>> isRight (refine @(FromTo 0 16) @Int 13)---   True------   >>> isRight (refine @(FromTo 13 15) @Int 13)---   True------   >>> isRight (refine @(FromTo 13 15) @Int 15)---   True------   >>> isLeft (refine @(FromTo 13 15) @Int 12)---   True-data FromTo (mn :: Nat) (mx :: Nat) = FromTo-  deriving (Generic)--instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx-         ) => Predicate (FromTo mn mx) x where-  validate p x = do-    let mn' = natVal (Proxy @mn)-    let mx' = natVal (Proxy @mx)-    unless ((x >= fromIntegral mn') && (x <= fromIntegral mx')) $ do-      let msg = [ "Value is out of range (minimum: "-                , PP.pretty mn'-                , ", maximum: "-                , PP.pretty mx'-                , ")"-                ] |> mconcat-      throwRefineOtherException (typeOf p) msg-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is equal to the specified---   type-level number @n@.------   >>> isRight (refine @(EqualTo 5) @Int 5)---   True------   >>> isLeft (refine @(EqualTo 6) @Int 5)---   True-data EqualTo (n :: Nat) = EqualTo-  deriving (Generic)--instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where-  validate p x = do-    let x' = natVal p-    unless (x == fromIntegral x') $ do-      throwRefineOtherException (typeOf p) ("Value does not equal " <> PP.pretty x')-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is not equal to the specified---   type-level number @n@.------   >>> isRight (refine @(NotEqualTo 6) @Int 5)---   True------   >>> isLeft (refine @(NotEqualTo 5) @Int 5)---   True--data NotEqualTo (n :: Nat) = NotEqualTo-  deriving (Generic)--instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where-  validate p x = do-    let x' = natVal p-    unless (x /= fromIntegral x') $ do-      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@.------   >>> isRight (refine @(NegativeFromTo 5 12) @Int (-3))---   True------   >>> isLeft (refine @(NegativeFromTo 4 3) @Int (-5))---   True-data NegativeFromTo (n :: Nat) (m :: Nat) = NegativeFromTo-  deriving (Generic)--instance (Ord x, Num x, KnownNat n, KnownNat 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 divisible by @n@.------   >>> isRight (refine @(DivisibleBy 3) @Int 12)---   True------   >>> isLeft (refine @(DivisibleBy 2) @Int 37)---   True-data DivisibleBy (n :: Nat) = DivisibleBy-  deriving (Generic)--instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where-  validate p x = unless (x `mod` (fromIntegral $ natVal p) == 0) $ do-    throwRefineOtherException (typeOf p) $ "Value is not divisible by " <> PP.pretty (natVal p)-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is odd.------   >>> isRight (refine @Odd @Int 33)---   True------   >>> isLeft (refine @Odd @Int 32)---   True-data Odd = Odd-  deriving (Generic)--instance (Integral x) => Predicate Odd x where-  validate p x = unless (odd x) $ do-    throwRefineOtherException (typeOf p) $ "Value is not odd."-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is even.------   >>> isRight (refine @Even @Int 32)---   True------   >>> isLeft (refine @Even @Int 33)---   True-data Even = Even-  deriving (Generic)--instance (Integral x) => Predicate Even x where-  validate p x = unless (even x) $ do-    throwRefineOtherException (typeOf p) $ "Value is not even."-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is greater than zero.-type Positive = GreaterThan 0---- | A 'Predicate' ensuring that the value is less than or equal to zero.-type NonPositive = To 0---- | A 'Predicate' ensuring that the value is less than zero.-type Negative = LessThan 0---- | A 'Predicate' ensuring that the value is greater than or equal to zero.-type NonNegative = From 0---- | An inclusive range of values from zero to one.-type ZeroToOne = FromTo 0 1---- | A 'Predicate' ensuring that the value is not equal to zero.-type NonZero = NotEqualTo 0---- | A 'Predicate' ensuring that the 'Foldable' is non-empty.-type NonEmpty = SizeGreaterThan 0-------------------------------------------------------------------------------------- |--- A typeclass containing "safe" conversions between refined predicates--- where the target is /weaker/ than the source: that is, all values that--- satisfy the first predicate will be guarunteed to satisy the second.------ Take care: writing an instance declaration for your custom predicates is--- the same as an assertion that 'weaken' is safe to use:------ @--- instance 'Weaken' Pred1 Pred2--- @------ For most of the instances, explicit type annotations for the result--- value's type might be required.-class Weaken from to where-  weaken :: Refined from x -> Refined to x-  weaken = coerce--instance (n <= m)         => Weaken (LessThan n)    (LessThan m)-instance (n <= m)         => Weaken (LessThan n)    (To m)-instance (n <= m)         => Weaken (To n)          (To m)-instance (m <= n)         => Weaken (GreaterThan n) (GreaterThan m)-instance (m <= n)         => Weaken (GreaterThan n) (From m)-instance (m <= n)         => Weaken (From n)        (From m)-instance (p <= n, m <= q) => Weaken (FromTo n m)    (FromTo p q)-instance (p <= n)         => Weaken (FromTo n m)    (From p)-instance (m <= q)         => Weaken (FromTo n m)    (To q)---- | This function helps type inference.---   It is equivalent to the following:------ @--- instance Weaken (And l r) l--- @-andLeft :: Refined (And l r) x -> Refined l x-andLeft = coerce---- | This function helps type inference.---   It is equivalent to the following:------ @--- instance Weaken (And l r) r--- @-andRight :: Refined (And l r) x -> Refined r x-andRight = coerce---- | This function helps type inference.---   It is equivalent to the following:------ @--- instance Weaken l (Or l r)--- @-leftOr :: Refined l x -> Refined (Or l r) x-leftOr = coerce---- | This function helps type inference.---   It is equivalent to the following:------ @--- instance Weaken r (Or l r)--- @-rightOr :: Refined r x -> Refined (Or l r) x-rightOr = coerce---- | Strengthen a refinement by composing it with another.-strengthen :: forall p p' x. (Predicate p x, Predicate p' x)-  => Refined p x-  -> Either RefineException (Refined (p && p') x)-strengthen r = refine @(p && p') (unrefine r)-{-# inlineable strengthen #-}---- | Strengthen a refinement by composing it with another---   inside of the 'RefineT' monad.-strengthenM :: forall p p' x m. (Predicate p x, Predicate p' x, Monad m)-  => Refined p x-  -> RefineT m (Refined (p && p') x)-strengthenM r = exceptRefine (strengthen r)-------------------------------------------------------------------------------------- | An exception encoding the way in which a 'Predicate' failed.-data RefineException-  = -- | A 'RefineException' for failures involving the 'Not' predicate.-    RefineNotException-    { _RefineException_typeRep   :: !TypeRep-      -- ^ The 'TypeRep' of the @'Not' p@ type.-    }--  | -- | A 'RefineException' for failures involving the 'And' predicate.-    RefineAndException-    { _RefineException_typeRep   :: !TypeRep-      -- ^ The 'TypeRep' of the @'And' l r@ type.-    , _RefineException_andChild  :: !(These RefineException RefineException)-      -- ^ A 'These' encoding which branch(es) of the 'And' failed:-      --   if the 'RefineException' came from the @l@ predicate, then-      --   this will be 'This', if it came from the @r@ predicate, this-      --   will be 'That', and if it came from both @l@ and @r@, this-      --   will be 'These'.--      -- note to self: what am I, Dr. Seuss?-    }--  | -- | A 'RefineException' for failures involving the 'Or' predicate.-    RefineOrException-    { _RefineException_typeRep   :: !TypeRep-      -- ^ The 'TypeRep' of the @'Or' l r@ type.-    , _RefineException_orLChild  :: !RefineException-      -- ^ The 'RefineException' for the @l@ failure.-    , _RefineException_orRChild  :: !RefineException-      -- ^ The 'RefineException' for the @l@ failure.-    }--  | -- | A 'RefineException' for failures involving all other predicates.-    RefineOtherException-    { _RefineException_typeRep   :: !TypeRep-      -- ^ The 'TypeRep' of the predicate that failed.-    , _RefineException_message  :: !(PP.Doc Void)-      -- ^ A custom message to display.-    }-  deriving (Generic)--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 = \case-  RefineOtherException tr msg ->-    [ "The predicate ("-    , PP.pretty (show tr)-    , ") does not hold: "-    , newline-    , twoSpaces-    , PP.pretty (show msg)-    ] |> mconcat-  RefineNotException tr ->-    [ "The negation of the predicate ("-    , PP.pretty (show tr)-    , ") does not hold:"-    , newline-    , twoSpaces-    ] |> 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-  pretty = displayRefineException---- | Encode a 'RefineException' for use with \Control.Exception\.-instance Exception RefineException where-  displayException = show-------------------------------------------------------------------------------------- | A monad transformer that adds @'RefineException'@s to other monads.------   The @'pure'@ and @'Control.Monad.return'@ functions yield computations that produce---   the given value, while @'>>='@ sequences two subcomputations, exiting---   on the first @'RefineException'@.-newtype RefineT m a-  = RefineT (ExceptT RefineException m a)-  deriving ( Functor, Applicative, Monad, MonadFix-           , MonadError RefineException, MonadTrans-           , Generic, Generic1-           )---- | The inverse of @'RefineT'@.-runRefineT-  :: RefineT m a-  -> m (Either RefineException a)-runRefineT = coerce .> ExceptT.runExceptT---- | Map the unwrapped computation using the given function.------   @'runRefineT' ('mapRefineT' f m) = f ('runRefineT' m)@-mapRefineT-  :: (m (Either RefineException a) -> n (Either RefineException b))-  -> RefineT m a-  -> RefineT n b-mapRefineT f = coerce .> ExceptT.mapExceptT f .> coerce-------------------------------------------------------------------------------------- | @'RefineM' a@ is equivalent to @'RefineT' 'Identity' a@ for any type @a@.-type RefineM a = RefineT Identity a---- | Constructs a computation in the 'RefineM' monad. (The inverse of @'runRefineM'@).-refineM-  :: Either RefineException a-  -> RefineM a-refineM = ExceptT.except .> (coerce :: ExceptT RefineException Identity a -> RefineM a)---- | Run a monadic action of type @'RefineM' a@,---   yielding an @'Either' 'RefineException' a@.------   This is just defined as @'runIdentity' '.' 'runRefineT'@.-runRefineM-  :: RefineM a-  -> Either RefineException a-runRefineM = runRefineT .> runIdentity-------------------------------------------------------------------------------------- | Constructor for computations in the @'RefineT'@ movie.---   (The inverse of 'runRefineT').-exceptRefine-  :: (Monad m)-  => Either RefineException a-  -> RefineT m a-exceptRefine = MonadError.liftEither---- | One can use @'throwRefine'@ inside of a monadic---   context to begin processing a @'RefineException'@.-throwRefine-  :: (Monad m)-  => RefineException-  -> RefineT m a-throwRefine = MonadError.throwError---- | A handler function to handle previous @'RefineException'@s---   and return to normal execution. A common idiom is:------   @ do { action1; action2; action3 } `'catchRefine'` handler @------   where the action functions can call @'throwRefine'@. Note that---   handler and the do-block must have the same return type.-catchRefine-  :: (Monad m)-  => RefineT m a-  -> (RefineException -> RefineT m a)-  -> RefineT m a-catchRefine = MonadError.catchError---- | A handler for a @'RefineException'@.------   'throwRefineOtherException' is useful for defining what---   behaviour 'validate' should have in the event of a predicate failure.-throwRefineOtherException-  :: (Monad m)-  => TypeRep-  -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'.-  -> PP.Doc Void-  -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed.-  -> RefineT m a-throwRefineOtherException rep-  = RefineOtherException rep .> throwRefine----------------------------------------------------------------------------------

@@ -1,44 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai------ 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 ()-----------------------------------------------------------------------------------

@@ -1,56 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai------ 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

@@ -1,91 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai------ 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 AllowAmbiguousTypes #-}-{-# LANGUAGE CPP                 #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}-------------------------------------------------------------------------------------- | 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, RefineException, Predicate, refine, reifyPredicate)-import           Refined.Unsafe   (reallyUnsafeRefine)-import           Test.QuickCheck  (Arbitrary(arbitrary), suchThatMaybe, Gen, sized, resize)-import           Data.Typeable    (Typeable, showsTypeRep, typeRep)-import           Data.Proxy       (Proxy(Proxy))------------------------------------------------------------------------------------instance forall p a. (Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) where-  arbitrary = loop 0 arbitrary--loop :: forall p a. (Typeable p, Typeable a, Predicate p a)-  => Int -> Gen a -> Gen (Refined p a)-loop runs gen-  | runs < 100 = do-      m <- suchThatRefined gen-      case m of-        Just x -> do-          pure x-        Nothing -> do-          loop (runs + 1) gen-  | otherwise = error (refinedGenError (Proxy @p) (Proxy @a))--refinedGenError :: (Typeable p, Typeable a)-  => Proxy p -> Proxy a -> String-refinedGenError p a = "arbitrary :: Refined ("-  ++ typeName p-  ++ ") ("-  ++ typeName a-  ++ "): Failed to generate a value that satisfied"-  ++ " the predicate after 100 tries."--suchThatRefined :: forall p a. (Predicate p a)-  => Gen a -> Gen (Maybe (Refined p a))-suchThatRefined gen = do-  m <- suchThatMaybe gen (reifyPredicate @p @a)-  case m of-    Nothing -> pure Nothing-    Just x -> pure (Just (reallyUnsafeRefine x))--typeName :: Typeable a => Proxy a -> String-typeName = flip showsTypeRep "" . typeRep------------------------------------------------------------------------------------#endif

@@ -2,7 +2,7 @@  -- Copyright © 2015 Nikita Volkov -- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai+-- Copyright © 2020 chessai -- -- Permission is hereby granted, free of charge, to any person -- obtaining a copy of this software and associated documentation@@ -27,239 +27,20 @@  -------------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE PackageImports #-}  -------------------------------------------------------------------------------- -{-# LANGUAGE CPP                #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE InstanceSigs       #-}+{-# OPTIONS_GHC -Wall #-}  -------------------------------------------------------------------------------- --- | 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.+-- | This module is deprecated. It will be removed in a future+--   release. Use the 'Data.These' module from the these-skinny+--   package instead. 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+  {-# DEPRECATED "This module will be removed in the next majour release. Use Data.These from the these-skinny package instead." #-}+  ( module Data.These   ) 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-+import "these-skinny" Data.These

@@ -2,7 +2,7 @@  -- Copyright © 2015 Nikita Volkov -- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai+-- Copyright © 2020 chessai -- -- Permission is hereby granted, free of charge, to any person -- obtaining a copy of this software and associated documentation@@ -59,14 +59,11 @@  -------------------------------------------------------------------------------- -import           Control.Exception            (Exception(displayException))+import           Control.Exception            (displayException) import           Data.Coerce                  (coerce)-import           Data.Either                  (either)-import           Data.Function                (id) -import           GHC.Err                      (error)--import           Refined.Internal             (Refined(Refined), Predicate, refine, (.>))+import           Refined                      (Predicate, refine)+import           Refined.Unsafe.Type          (Refined(Refined)) import           Data.Type.Coercion           (Coercion (..)) #if __GLASGOW_HASKELL__ >= 805 import           Data.Coerce                  (Coercible)@@ -79,25 +76,34 @@ --   does not satisfy the predicate. -- --   WARNING: this function is not total!+--+--   @since 0.2.0.0 unsafeRefine :: (Predicate p x) => x -> Refined p x-unsafeRefine = refine .> either (displayException .> error) id+unsafeRefine = either (error . displayException) id . refine {-# INLINABLE unsafeRefine #-}  -- | Constructs a 'Refined' value, completely --   ignoring any refinements! Use this only --   when you can manually prove that the refinement --   holds.+--+--   @since 0.3.0.0 reallyUnsafeRefine :: x -> Refined p x reallyUnsafeRefine = coerce {-# INLINE reallyUnsafeRefine #-}  -- | A coercion between a type and any refinement of that type.--- See "Data.Type.Coercion" for functions manipulating coercions.+--   See "Data.Type.Coercion" for functions manipulating+--   coercions.+--+--   @since 0.3.0.0 reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x) reallyUnsafeUnderlyingRefined = Coercion --- | A coercion between two 'Refined' types, magicking up the claim--- that one predicate is entirely equivalent to another.+-- | A coercion between two 'Refined' types, magicking up the+--   claim that one predicate is entirely equivalent to another.+--+--   @since 0.3.0.0 reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x) reallyUnsafePredEquiv = Coercion -- Note: reallyUnsafePredEquiv =@@ -113,6 +119,8 @@ -- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x) -- reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion -- @+--+--   @since 0.3.0.0 reallyUnsafeAllUnderlyingRefined   :: ((forall x y p. (Coercible x y => Coercible y (Refined p x))) => r) -> r -- Why is this constraint so convoluted? Because otherwise the constraint

@@ -2,7 +2,7 @@  -- Copyright © 2015 Nikita Volkov -- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai+-- Copyright © 2020 chessai -- -- Permission is hereby granted, free of charge, to any person -- obtaining a copy of this software and associated documentation@@ -27,12 +27,17 @@  -------------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE DeriveFoldable             #-}+{-# LANGUAGE DerivingStrategies         #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RoleAnnotations            #-}+{-# LANGUAGE TemplateHaskell            #-}  --------------------------------------------------------------------------------  -- | This module exports the 'Refined' type with its---   constructor. This is very risky! In particular, the 'Coercible'+--   constructor. This is very risky! In particular, the 'Data.Coerce.Coercible' --   instances will be visible throughout the importing module. --   It is usually better to build the necessary coercions locally --   using the utilities in "Refined.Unsafe", but in some cases@@ -42,4 +47,33 @@   ( Refined(Refined)   ) where -import Refined.Internal (Refined(Refined))+import           Control.DeepSeq              (NFData)+import qualified Language.Haskell.TH.Syntax   as TH++-- | A refinement type, which wraps a value of type @x@.+--+--   @since 0.1.0.0+newtype Refined p x+  = Refined x -- ^ @since 0.1.0.0+  deriving newtype+    ( Eq -- ^ @since 0.1.0.0+    , Ord -- ^ @since 0.1.0.0+    , NFData -- ^ @since 0.5+    )+  deriving stock+    ( Show -- ^ @since 0.1.0.0+    )+  deriving stock+    ( Foldable -- ^ @since 0.2+    )++-- | @since 0.3.0.0+type role Refined nominal nominal++-- | @since 0.1.0.0+instance (TH.Lift x) => TH.Lift (Refined p x) where+  lift (Refined a) = [|Refined a|]+#if MIN_VERSION_template_haskell(2,16,0)+  liftTyped (Refined a) = [||Refined a||]+#endif+

@@ -10,16 +10,11 @@ module Main (main) where  import Refined-import Prelude (IO,putStrLn,Int) 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)  id_   = $$(refineTH_ @IdPred     @Int 3) even_ = $$(refineTH_ @(Not Even) @Int 3)

@@ -8,10 +8,6 @@ srcFiles :: [String] srcFiles =   [ "src/Refined.hs"-  , "src/Refined/Internal.hs"-  , "src/Refined/Orphan/Aeson.hs"-  , "src/Refined/Orphan/QuickCheck.hs"-  , "src/Refined/Orphan.hs"   , "src/Refined/These.hs"   , "src/Refined/Unsafe/Type.hs"   , "src/Refined/Unsafe.hs"

@@ -11,7 +11,6 @@  import Test.QuickCheck import Refined-import Refined.Orphan  main :: IO () main = mapM_ quickCheck