diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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/ diff --git a/changelog.md b/changelog.md new file mode 100644 --- /dev/null +++ b/changelog.md @@ -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 diff --git a/refined.cabal b/refined.cabal --- a/refined.cabal +++ b/refined.cabal @@ -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 diff --git a/src/Refined.hs b/src/Refined.hs --- a/src/Refined.hs +++ b/src/Refined.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 +-- > :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 +-- . +-- +-- @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 + -- + -- 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 diff --git a/src/Refined/Internal.hs b/src/Refined/Internal.hs deleted file mode 100644 --- a/src/Refined/Internal.hs +++ /dev/null @@ -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 --- > :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 - --------------------------------------------------------------------------------- diff --git a/src/Refined/Orphan.hs b/src/Refined/Orphan.hs deleted file mode 100644 --- a/src/Refined/Orphan.hs +++ /dev/null @@ -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 () - --------------------------------------------------------------------------------- - diff --git a/src/Refined/Orphan/Aeson.hs b/src/Refined/Orphan/Aeson.hs deleted file mode 100644 --- a/src/Refined/Orphan/Aeson.hs +++ /dev/null @@ -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 diff --git a/src/Refined/Orphan/QuickCheck.hs b/src/Refined/Orphan/QuickCheck.hs deleted file mode 100644 --- a/src/Refined/Orphan/QuickCheck.hs +++ /dev/null @@ -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 diff --git a/src/Refined/These.hs b/src/Refined/These.hs --- a/src/Refined/These.hs +++ b/src/Refined/These.hs @@ -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 diff --git a/src/Refined/Unsafe.hs b/src/Refined/Unsafe.hs --- a/src/Refined/Unsafe.hs +++ b/src/Refined/Unsafe.hs @@ -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 diff --git a/src/Refined/Unsafe/Type.hs b/src/Refined/Unsafe/Type.hs --- a/src/Refined/Unsafe/Type.hs +++ b/src/Refined/Unsafe/Type.hs @@ -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 + diff --git a/test/Compiles.hs b/test/Compiles.hs --- a/test/Compiles.hs +++ b/test/Compiles.hs @@ -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) diff --git a/test/Doctests.hs b/test/Doctests.hs --- a/test/Doctests.hs +++ b/test/Doctests.hs @@ -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" diff --git a/test/QuickCheck.hs b/test/QuickCheck.hs --- a/test/QuickCheck.hs +++ b/test/QuickCheck.hs @@ -11,7 +11,6 @@ import Test.QuickCheck import Refined -import Refined.Orphan main :: IO () main = mapM_ quickCheck