-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Refinement types with static and runtime checking
--   
--   For an extensive introduction to the library please follow to <a>this
--   blog-post</a>.
@package refined
@version 0.4.2


-- | This module is defined internally to avoid using the <a>these</a>
--   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 <a>These</a> type here. If one should need a fuller API, see
--   <a>https://hackage.haskell.org/package/these</a> Converting to/from
--   the two types should be trivial, as the data constructors are exported
--   from both.
module Refined.These

-- | This is defined internally to avoid using the <a>these</a> 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 -> These a b
That :: b -> These a b
These :: a -> b -> These a b

-- | Case analysis for the <a>These</a> type.
these :: (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c

-- | Takes two default values and produces a tuple.
fromThese :: a -> b -> These a b -> (a, b)

-- | Coalesce with the provided operation.
mergeThese :: (a -> a -> a) -> These a a -> a

-- | BiMap and coalesce results with the provided operation.
mergeTheseWith :: (a -> c) -> (b -> c) -> (c -> c -> c) -> These a b -> c

-- | A <tt>Traversal</tt> of the first half of a <a>These</a>, suitable for
--   use with <tt>Control.Lens</tt>.
here :: Applicative f => (a -> f b) -> These a t -> f (These b t)

-- | A <tt>Traversal</tt> of the second half of a <a>These</a>, suitable
--   for use with <tt>Control.Lens</tt>.
there :: Applicative f => (a -> f b) -> These t a -> f (These t b)

-- | <pre>
--   <a>justThis</a> = <a>these</a> <a>Just</a> (_ -&gt; <a>Nothing</a>) (_ _ -&gt; <a>Nothing</a>)
--   </pre>
justThis :: These a b -> Maybe a

-- | <pre>
--   <a>justThat</a> = <a>these</a> (_ -&gt; <a>Nothing</a>) <a>Just</a> (_ _ -&gt; <a>Nothing</a>)
--   </pre>
justThat :: These a b -> Maybe b

-- | <pre>
--   <a>justThese</a> = <a>these</a> (_ -&gt; <a>Nothing</a>) (_ -&gt; <a>Nothing</a>) (a b -&gt; <a>Just</a> (a, b))
--   </pre>
justThese :: These a b -> Maybe (a, b)

-- | Select all <a>This</a> constructors from a list.
catThis :: [These a b] -> [a]

-- | Select all <a>That</a> constructors from a list.
catThat :: [These a b] -> [b]

-- | Select all <a>These</a> constructors from a list.
catThese :: [These a b] -> [(a, b)]

-- | Select each constructor and partition them into separate lists.
partitionThese :: [These a b] -> ([(a, b)], ([a], [b]))

-- | <pre>
--   <a>isThis</a> = <a>isJust</a> . <a>justThis</a>
--   </pre>
isThis :: These a b -> Bool

-- | <pre>
--   <a>isThat</a> = <a>isJust</a> . <a>justThat</a>
--   </pre>
isThat :: These a b -> Bool

-- | <pre>
--   <a>isThese</a> = <a>isJust</a> . <a>justThese</a>
--   </pre>
isThese :: These a b -> Bool

-- | <a>Bifunctor</a> map.
mapThese :: (a -> c) -> (b -> d) -> These a b -> These c d

-- | <pre>
--   <a>mapThis</a> = over <a>here</a>
--   </pre>
mapThis :: (a -> c) -> These a b -> These c b

-- | <pre>
--   <a>mapThat</a> = over <a>there</a>
--   </pre>
mapThat :: (b -> d) -> These a b -> These a d
instance GHC.Generics.Generic1 (Refined.These.These a)
instance GHC.Generics.Generic (Refined.These.These a b)
instance (Data.Data.Data a, Data.Data.Data b) => Data.Data.Data (Refined.These.These a b)
instance (GHC.Show.Show a, GHC.Show.Show b) => GHC.Show.Show (Refined.These.These a b)
instance (GHC.Read.Read a, GHC.Read.Read b) => GHC.Read.Read (Refined.These.These a b)
instance (GHC.Classes.Ord a, GHC.Classes.Ord b) => GHC.Classes.Ord (Refined.These.These a b)
instance (GHC.Classes.Eq a, GHC.Classes.Eq b) => GHC.Classes.Eq (Refined.These.These a b)
instance (GHC.Base.Semigroup a, GHC.Base.Semigroup b) => GHC.Base.Semigroup (Refined.These.These a b)
instance Data.Bifunctor.Bifunctor Refined.These.These
instance GHC.Base.Functor (Refined.These.These a)
instance GHC.Base.Semigroup a => GHC.Base.Applicative (Refined.These.These a)
instance GHC.Base.Semigroup a => GHC.Base.Monad (Refined.These.These a)
instance (Control.DeepSeq.NFData a, Control.DeepSeq.NFData b) => Control.DeepSeq.NFData (Refined.These.These a b)
instance Data.Foldable.Foldable (Refined.These.These a)
instance Data.Traversable.Traversable (Refined.These.These a)
instance Data.Bifoldable.Bifoldable Refined.These.These


-- | 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 <a>Refined</a> type. A <a>Refined</a> <tt>p</tt> <tt>x</tt> wraps
--   a value of type <tt>x</tt>, ensuring that it satisfies a type-level
--   predicate <tt>p</tt>.
--   
--   A simple introduction to this library can be found here:
--   <a>http://nikita-volkov.github.io/refined/</a>
module Refined.Internal

-- | A refinement type, which wraps a value of type <tt>x</tt>, ensuring
--   that it satisfies a type-level predicate <tt>p</tt>.
newtype Refined p x
Refined :: x -> Refined p x

-- | A smart constructor of a <a>Refined</a> value. Checks the input value
--   at runtime.
refine :: Predicate p x => x -> Either RefineException (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling <a>throwM</a>
--   if the value does not satisfy the predicate.
refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling <a>fail</a> if
--   the value does not satisfy the predicate.
refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling
--   <a>throwError</a> if the value does not satisfy the predicate.
refineError :: (Predicate p x, MonadError RefineException m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at compile-time using
--   <tt>-XTemplateHaskell</tt>.
--   
--   For example:
--   
--   <pre>
--   $$(refineTH 23) :: Refined Positive Int
--   Refined 23
--   </pre>
--   
--   Here's an example of an invalid value:
--   
--   <pre>
--   $$(refineTH 0) :: Refined Positive Int
--   &lt;interactive&gt;: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
--   </pre>
--   
--   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
--   <a>https://hackage.haskell.org/package/th-lift-instances/</a>
refineTH :: (Predicate p x, Lift x) => x -> Q (TExp (Refined p x))

-- | Extracts the refined value.
unrefine :: Refined p x -> x

-- | A typeclass which defines a runtime interpretation of a type-level
--   predicate <tt>p</tt> for type <tt>x</tt>.
class (Typeable p) => Predicate p x

-- | Check the value <tt>x</tt> according to the predicate <tt>p</tt>,
--   producing an error string if the value does not satisfy.
validate :: (Predicate p x, Monad m) => p -> x -> RefineT m ()

-- | The negation of a predicate.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(Not NonEmpty) @[Int] [])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(Not NonEmpty) @[Int] [1,2])
--   True
--   </pre>
data Not p
Not :: Not p

-- | The conjunction of two predicates.
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(And Positive Negative) @Int 3)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(And Positive Odd) @Int 203)
--   True
--   </pre>
data And l r
And :: And l r

-- | The conjunction of two predicates.
type (&&) = And
infixr 3 &&

-- | The disjunction of two predicates.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(Or Even Odd) @Int 3)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)
--   True
--   </pre>
data Or l r
Or :: Or l r

-- | The disjunction of two predicates.
type (||) = Or
infixr 2 ||

-- | A predicate which is satisfied for all types. The value is not
--   evaluated by <a>validate</a>.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @IdPred @Int undefined)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @IdPred @Int undefined)
--   False
--   </pre>
data IdPred
IdPred :: IdPred

-- | A <a>Predicate</a> ensuring that the value is less than the specified
--   type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(LessThan 12) @Int 11)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(LessThan 12) @Int 12)
--   True
--   </pre>
data LessThan (n :: Nat)
LessThan :: LessThan

-- | A <a>Predicate</a> ensuring that the value is greater than the
--   specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(GreaterThan 65) @Int 67)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(GreaterThan 65) @Int 65)
--   True
--   </pre>
data GreaterThan (n :: Nat)
GreaterThan :: GreaterThan

-- | A <a>Predicate</a> ensuring that the value is greater than or equal to
--   the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(From 9) @Int 10)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(From 10) @Int 10)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(From 11) @Int 10)
--   True
--   </pre>
data From (n :: Nat)
From :: From

-- | A <a>Predicate</a> ensuring that the value is less than or equal to
--   the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(To 23) @Int 17)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(To 17) @Int 23)
--   True
--   </pre>
data To (n :: Nat)
To :: To

-- | A <a>Predicate</a> ensuring that the value is within an inclusive
--   range.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(FromTo 0 16) @Int 13)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(FromTo 13 15) @Int 13)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(FromTo 13 15) @Int 15)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(FromTo 13 15) @Int 12)
--   True
--   </pre>
data FromTo (mn :: Nat) (mx :: Nat)
FromTo :: FromTo

-- | A <a>Predicate</a> ensuring that the value is greater or equal than a
--   negative number specified as a type-level (positive) number <tt>n</tt>
--   and less than a type-level (positive) number <tt>m</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(NegativeFromTo 5 12) @Int (-3))
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(NegativeFromTo 4 3) @Int (-5))
--   True
--   </pre>
data NegativeFromTo (n :: Nat) (m :: Nat)
NegativeFromTo :: NegativeFromTo

-- | A <a>Predicate</a> ensuring that the value is equal to the specified
--   type-level number <tt>n</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(EqualTo 5) @Int 5)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(EqualTo 6) @Int 5)
--   True
--   </pre>
data EqualTo (n :: Nat)
EqualTo :: EqualTo

-- | A <a>Predicate</a> ensuring that the value is not equal to the
--   specified type-level number <tt>n</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(NotEqualTo 6) @Int 5)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(NotEqualTo 5) @Int 5)
--   True
--   </pre>
data NotEqualTo (n :: Nat)
NotEqualTo :: NotEqualTo

-- | A <a>Predicate</a> ensuring that the value is odd.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @Odd @Int 33)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @Odd @Int 32)
--   True
--   </pre>
data Odd
Odd :: Odd

-- | A <a>Predicate</a> ensuring that the value is even.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @Even @Int 32)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @Even @Int 33)
--   True
--   </pre>
data Even
Even :: Even

-- | A <a>Predicate</a> ensuring that the value is divisible by <tt>n</tt>.
--   That is to say, <tt>m <a>mod</a> <a>natVal</a> (<a>Proxy</a> </tt>n)
--   <a>==</a> 0@
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(DivisibleBy 3) @Int 12)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(DivisibleBy 2) @Int 37)
--   True
--   </pre>
data DivisibleBy (n :: Nat)
DivisibleBy :: DivisibleBy

-- | A <a>Predicate</a> ensuring that the value is greater than zero.
type Positive = GreaterThan 0

-- | A <a>Predicate</a> ensuring that the value is less than or equal to
--   zero.
type NonPositive = To 0

-- | A <a>Predicate</a> ensuring that the value is less than zero.
type Negative = LessThan 0

-- | A <a>Predicate</a> 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 <a>Predicate</a> ensuring that the value is not equal to zero.
type NonZero = NotEqualTo 0

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is less than the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])
--   True
--   </pre>
data SizeLessThan (n :: Nat)
SizeLessThan :: SizeLessThan

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is greater than the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine  @(SizeGreaterThan 3) @[Int] [1,2,3])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])
--   True
--   </pre>
data SizeGreaterThan (n :: Nat)
SizeGreaterThan :: SizeGreaterThan

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is equal to the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])
--   True
--   </pre>
data SizeEqualTo (n :: Nat)
SizeEqualTo :: SizeEqualTo

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> is non-empty.
type NonEmpty = SizeGreaterThan 0

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> contains elements
--   in a strictly ascending order.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])
--   True
--   </pre>
data Ascending
Ascending :: Ascending

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> contains elements
--   in a strictly descending order.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])
--   True
--   </pre>
data Descending
Descending :: Descending

-- | A typeclass containing "safe" conversions between refined predicates
--   where the target is <i>weaker</i> 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 <a>weaken</a> is safe to use:
--   
--   <pre>
--   instance <a>Weaken</a> Pred1 Pred2
--   </pre>
--   
--   For most of the instances, explicit type annotations for the result
--   value's type might be required.
class Weaken from to
weaken :: Weaken from to => Refined from x -> Refined to x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken (And l r) l
--   </pre>
andLeft :: Refined (And l r) x -> Refined l x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken (And l r) r
--   </pre>
andRight :: Refined (And l r) x -> Refined r x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken l (Or l r)
--   </pre>
leftOr :: Refined l x -> Refined (Or l r) x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken r (Or l r)
--   </pre>
rightOr :: Refined r x -> Refined (Or l r) x

-- | An exception encoding the way in which a <a>Predicate</a> failed.
data RefineException

-- | A <a>RefineException</a> for failures involving the <a>Not</a>
--   predicate.
RefineNotException :: !TypeRep -> RefineException

-- | A <a>RefineException</a> for failures involving the <a>And</a>
--   predicate.
RefineAndException :: !TypeRep -> !These RefineException RefineException -> RefineException

-- | A <a>RefineException</a> for failures involving the <a>Or</a>
--   predicate.
RefineOrException :: !TypeRep -> !RefineException -> !RefineException -> RefineException

-- | A <a>RefineException</a> for failures involving all other predicates.
RefineOtherException :: !TypeRep -> !Doc Void -> RefineException

-- | Display a <a>RefineException</a> as a <tt><a>Doc</a> ann</tt>
displayRefineException :: RefineException -> Doc ann

-- | A monad transformer that adds <tt><a>RefineException</a></tt>s to
--   other monads.
--   
--   The <tt><a>pure</a></tt> and <tt><a>return</a></tt> functions yield
--   computations that produce the given value, while
--   <tt><tt>&gt;&gt;=</tt></tt> sequences two subcomputations, exiting on
--   the first <tt><a>RefineException</a></tt>.
data RefineT m a

-- | The inverse of <tt><a>RefineT</a></tt>.
runRefineT :: RefineT m a -> m (Either RefineException a)

-- | Map the unwrapped computation using the given function.
--   
--   <pre>
--   <a>runRefineT</a> (<a>mapRefineT</a> f m) = f (<a>runRefineT</a> m)
--   </pre>
mapRefineT :: (m (Either RefineException a) -> n (Either RefineException b)) -> RefineT m a -> RefineT n b

-- | <tt><a>RefineM</a> a</tt> is equivalent to <tt><a>RefineT</a>
--   <a>Identity</a> a</tt> for any type <tt>a</tt>.
type RefineM a = RefineT Identity a

-- | Constructs a computation in the <a>RefineM</a> monad. (The inverse of
--   <tt><a>runRefineM</a></tt>).
refineM :: Either RefineException a -> RefineM a

-- | Run a monadic action of type <tt><a>RefineM</a> a</tt>, yielding an
--   <tt><a>Either</a> <a>RefineException</a> a</tt>.
--   
--   This is just defined as <tt><a>runIdentity</a> <a>.</a>
--   <a>runRefineT</a></tt>.
runRefineM :: RefineM a -> Either RefineException a

-- | One can use <tt><a>throwRefine</a></tt> inside of a monadic context to
--   begin processing a <tt><a>RefineException</a></tt>.
throwRefine :: Monad m => RefineException -> RefineT m a

-- | A handler function to handle previous <tt><a>RefineException</a></tt>s
--   and return to normal execution. A common idiom is:
--   
--   <pre>
--   do { action1; action2; action3 } `<tt>catchRefine'</tt> handler
--   </pre>
--   
--   where the action functions can call <tt><a>throwRefine</a></tt>. 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

-- | A handler for a <tt><a>RefineException</a></tt>.
--   
--   <a>throwRefineOtherException</a> is useful for defining what behaviour
--   <a>validate</a> should have in the event of a predicate failure.
throwRefineOtherException :: Monad m => TypeRep -> Doc Void -> RefineT m a

-- | Helper function, stolen from the <tt>flow</tt> package.
(|>) :: a -> (a -> b) -> b
infixl 0 |>

-- | Helper function, stolen from the <tt>flow</tt> package.
(.>) :: (a -> b) -> (b -> c) -> a -> c
infixl 9 .>

-- | <pre>
--   &gt;&gt;&gt; pretty 1 &lt;+&gt; pretty "hello" &lt;+&gt; pretty 1.234
--   1 hello 1.234
--   </pre>
pretty :: Pretty a => a -> Doc ann
instance GHC.Generics.Generic1 (Refined.Internal.RefineT m)
instance GHC.Generics.Generic (Refined.Internal.RefineT m a)
instance Control.Monad.Trans.Class.MonadTrans Refined.Internal.RefineT
instance GHC.Base.Monad m => Control.Monad.Error.Class.MonadError Refined.Internal.RefineException (Refined.Internal.RefineT m)
instance Control.Monad.Fix.MonadFix m => Control.Monad.Fix.MonadFix (Refined.Internal.RefineT m)
instance GHC.Base.Monad m => GHC.Base.Monad (Refined.Internal.RefineT m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Refined.Internal.RefineT m)
instance GHC.Base.Functor m => GHC.Base.Functor (Refined.Internal.RefineT m)
instance GHC.Generics.Generic Refined.Internal.RefineException
instance GHC.Generics.Generic Refined.Internal.Even
instance GHC.Generics.Generic Refined.Internal.Odd
instance GHC.Generics.Generic (Refined.Internal.DivisibleBy n)
instance GHC.Generics.Generic (Refined.Internal.NegativeFromTo n m)
instance GHC.Generics.Generic (Refined.Internal.NotEqualTo n)
instance GHC.Generics.Generic (Refined.Internal.EqualTo n)
instance GHC.Generics.Generic (Refined.Internal.FromTo mn mx)
instance GHC.Generics.Generic (Refined.Internal.To n)
instance GHC.Generics.Generic (Refined.Internal.From n)
instance GHC.Generics.Generic (Refined.Internal.GreaterThan n)
instance GHC.Generics.Generic (Refined.Internal.LessThan n)
instance GHC.Generics.Generic Refined.Internal.Descending
instance GHC.Generics.Generic Refined.Internal.Ascending
instance GHC.Generics.Generic (Refined.Internal.SizeEqualTo n)
instance GHC.Generics.Generic (Refined.Internal.SizeGreaterThan n)
instance GHC.Generics.Generic (Refined.Internal.SizeLessThan n)
instance GHC.Generics.Generic1 (Refined.Internal.Or l)
instance GHC.Generics.Generic (Refined.Internal.Or l r)
instance GHC.Generics.Generic1 (Refined.Internal.And l)
instance GHC.Generics.Generic (Refined.Internal.And l r)
instance GHC.Generics.Generic1 Refined.Internal.Not
instance GHC.Generics.Generic (Refined.Internal.Not p)
instance GHC.Generics.Generic Refined.Internal.IdPred
instance GHC.Show.Show x => GHC.Show.Show (Refined.Internal.Refined p x)
instance GHC.Classes.Ord x => GHC.Classes.Ord (Refined.Internal.Refined p x)
instance Data.Foldable.Foldable (Refined.Internal.Refined p)
instance GHC.Classes.Eq x => GHC.Classes.Eq (Refined.Internal.Refined p x)
instance (GHC.Read.Read x, Refined.Internal.Predicate p x) => GHC.Read.Read (Refined.Internal.Refined p x)
instance Refined.Internal.Predicate Refined.Internal.IdPred x
instance (Refined.Internal.Predicate p x, Data.Typeable.Internal.Typeable p) => Refined.Internal.Predicate (Refined.Internal.Not p) x
instance (Refined.Internal.Predicate l x, Refined.Internal.Predicate r x, Data.Typeable.Internal.Typeable l, Data.Typeable.Internal.Typeable r) => Refined.Internal.Predicate (Refined.Internal.And l r) x
instance (Refined.Internal.Predicate l x, Refined.Internal.Predicate r x, Data.Typeable.Internal.Typeable l, Data.Typeable.Internal.Typeable r) => Refined.Internal.Predicate (Refined.Internal.Or l r) x
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.SizeLessThan n) (t a)
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.SizeGreaterThan n) (t a)
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.SizeEqualTo n) (t a)
instance (Data.Foldable.Foldable t, GHC.Classes.Ord a) => Refined.Internal.Predicate Refined.Internal.Ascending (t a)
instance (Data.Foldable.Foldable t, GHC.Classes.Ord a) => Refined.Internal.Predicate Refined.Internal.Descending (t a)
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.LessThan n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.GreaterThan n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.From n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.To n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat mn, GHC.TypeNats.KnownNat mx, mn GHC.TypeNats.<= mx) => Refined.Internal.Predicate (Refined.Internal.FromTo mn mx) x
instance (GHC.Classes.Eq x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.EqualTo n) x
instance (GHC.Classes.Eq x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.NotEqualTo n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => Refined.Internal.Predicate (Refined.Internal.NegativeFromTo n m) x
instance (GHC.Real.Integral x, GHC.TypeNats.KnownNat n) => Refined.Internal.Predicate (Refined.Internal.DivisibleBy n) x
instance GHC.Real.Integral x => Refined.Internal.Predicate Refined.Internal.Odd x
instance GHC.Real.Integral x => Refined.Internal.Predicate Refined.Internal.Even x
instance GHC.Show.Show Refined.Internal.RefineException
instance Data.Text.Prettyprint.Doc.Internal.Pretty Refined.Internal.RefineException
instance GHC.Exception.Type.Exception Refined.Internal.RefineException
instance (n GHC.TypeNats.<= m) => Refined.Internal.Weaken (Refined.Internal.LessThan n) (Refined.Internal.LessThan m)
instance (n GHC.TypeNats.<= m) => Refined.Internal.Weaken (Refined.Internal.LessThan n) (Refined.Internal.To m)
instance (n GHC.TypeNats.<= m) => Refined.Internal.Weaken (Refined.Internal.To n) (Refined.Internal.To m)
instance (m GHC.TypeNats.<= n) => Refined.Internal.Weaken (Refined.Internal.GreaterThan n) (Refined.Internal.GreaterThan m)
instance (m GHC.TypeNats.<= n) => Refined.Internal.Weaken (Refined.Internal.GreaterThan n) (Refined.Internal.From m)
instance (m GHC.TypeNats.<= n) => Refined.Internal.Weaken (Refined.Internal.From n) (Refined.Internal.From m)
instance (p GHC.TypeNats.<= n, m GHC.TypeNats.<= q) => Refined.Internal.Weaken (Refined.Internal.FromTo n m) (Refined.Internal.FromTo p q)
instance (p GHC.TypeNats.<= n) => Refined.Internal.Weaken (Refined.Internal.FromTo n m) (Refined.Internal.From p)
instance (m GHC.TypeNats.<= q) => Refined.Internal.Weaken (Refined.Internal.FromTo n m) (Refined.Internal.To q)
instance Language.Haskell.TH.Syntax.Lift x => Language.Haskell.TH.Syntax.Lift (Refined.Internal.Refined p x)


-- | This module exposes orphan instances for the <a>Refined</a> type. This
--   is unavoidable given the current module structure.
module Refined.Orphan.QuickCheck
instance (Test.QuickCheck.Arbitrary.Arbitrary a, Refined.Internal.Predicate p a) => Test.QuickCheck.Arbitrary.Arbitrary (Refined.Internal.Refined p a)


-- | This module exposes orphan instances for the <a>Refined</a> type. This
--   is unavoidable given the current module structure.
module Refined.Orphan.Aeson
instance (Data.Aeson.Types.FromJSON.FromJSON a, Refined.Internal.Predicate p a) => Data.Aeson.Types.FromJSON.FromJSON (Refined.Internal.Refined p a)
instance (Data.Aeson.Types.ToJSON.ToJSON a, Refined.Internal.Predicate p a) => Data.Aeson.Types.ToJSON.ToJSON (Refined.Internal.Refined p a)


-- | This module exposes orphan instances for the <tt>Refined</tt> type.
--   This is unavoidable given the current module structure.
module Refined.Orphan


-- | 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 <a>Refined</a> type. A <a>Refined</a> <tt>p</tt> <tt>x</tt> wraps
--   a value of type <tt>x</tt>, ensuring that it satisfies a type-level
--   predicate <tt>p</tt>.
--   
--   A simple introduction to this library can be found here:
--   <a>http://nikita-volkov.github.io/refined/</a>
--   
--   This module only provides <i>safe</i> constructions of <a>Refined</a>
--   values, <i>safe</i> meaning that the refinement predicate holds, and
--   the construction of the <a>Refined</a> 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 <i>Refined.Unsafe</i>.
module Refined

-- | A refinement type, which wraps a value of type <tt>x</tt>, ensuring
--   that it satisfies a type-level predicate <tt>p</tt>.
data Refined p x

-- | A smart constructor of a <a>Refined</a> value. Checks the input value
--   at runtime.
refine :: Predicate p x => x -> Either RefineException (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling <a>throwM</a>
--   if the value does not satisfy the predicate.
refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling <a>fail</a> if
--   the value does not satisfy the predicate.
refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at run-time, calling
--   <a>throwError</a> if the value does not satisfy the predicate.
refineError :: (Predicate p x, MonadError RefineException m) => x -> m (Refined p x)

-- | Constructs a <a>Refined</a> value at compile-time using
--   <tt>-XTemplateHaskell</tt>.
--   
--   For example:
--   
--   <pre>
--   $$(refineTH 23) :: Refined Positive Int
--   Refined 23
--   </pre>
--   
--   Here's an example of an invalid value:
--   
--   <pre>
--   $$(refineTH 0) :: Refined Positive Int
--   &lt;interactive&gt;: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
--   </pre>
--   
--   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
--   <a>https://hackage.haskell.org/package/th-lift-instances/</a>
refineTH :: (Predicate p x, Lift x) => x -> Q (TExp (Refined p x))

-- | Extracts the refined value.
unrefine :: Refined p x -> x

-- | A typeclass which defines a runtime interpretation of a type-level
--   predicate <tt>p</tt> for type <tt>x</tt>.
class (Typeable p) => Predicate p x

-- | Check the value <tt>x</tt> according to the predicate <tt>p</tt>,
--   producing an error string if the value does not satisfy.
validate :: (Predicate p x, Monad m) => p -> x -> RefineT m ()

-- | The negation of a predicate.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(Not NonEmpty) @[Int] [])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(Not NonEmpty) @[Int] [1,2])
--   True
--   </pre>
data Not p

-- | The conjunction of two predicates.
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(And Positive Negative) @Int 3)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(And Positive Odd) @Int 203)
--   True
--   </pre>
data And l r

-- | The conjunction of two predicates.
type (&&) = And
infixr 3 &&

-- | The disjunction of two predicates.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(Or Even Odd) @Int 3)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)
--   True
--   </pre>
data Or l r

-- | The disjunction of two predicates.
type (||) = Or
infixr 2 ||

-- | A predicate which is satisfied for all types. The value is not
--   evaluated by <a>validate</a>.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @IdPred @Int undefined)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @IdPred @Int undefined)
--   False
--   </pre>
data IdPred

-- | A <a>Predicate</a> ensuring that the value is less than the specified
--   type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(LessThan 12) @Int 11)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(LessThan 12) @Int 12)
--   True
--   </pre>
data LessThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than the
--   specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(GreaterThan 65) @Int 67)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(GreaterThan 65) @Int 65)
--   True
--   </pre>
data GreaterThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than or equal to
--   the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(From 9) @Int 10)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(From 10) @Int 10)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(From 11) @Int 10)
--   True
--   </pre>
data From (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is less than or equal to
--   the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(To 23) @Int 17)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(To 17) @Int 23)
--   True
--   </pre>
data To (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is within an inclusive
--   range.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(FromTo 0 16) @Int 13)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(FromTo 13 15) @Int 13)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(FromTo 13 15) @Int 15)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(FromTo 13 15) @Int 12)
--   True
--   </pre>
data FromTo (mn :: Nat) (mx :: Nat)

-- | A <a>Predicate</a> ensuring that the value is equal to the specified
--   type-level number <tt>n</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(EqualTo 5) @Int 5)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(EqualTo 6) @Int 5)
--   True
--   </pre>
data EqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is not equal to the
--   specified type-level number <tt>n</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(NotEqualTo 6) @Int 5)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(NotEqualTo 5) @Int 5)
--   True
--   </pre>
data NotEqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than zero.
type Positive = GreaterThan 0

-- | A <a>Predicate</a> ensuring that the value is less than or equal to
--   zero.
type NonPositive = To 0

-- | A <a>Predicate</a> ensuring that the value is less than zero.
type Negative = LessThan 0

-- | A <a>Predicate</a> 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 <a>Predicate</a> ensuring that the value is not equal to zero.
type NonZero = NotEqualTo 0

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is less than the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])
--   True
--   </pre>
data SizeLessThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is greater than the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine  @(SizeGreaterThan 3) @[Int] [1,2,3])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])
--   True
--   </pre>
data SizeGreaterThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is equal to the specified type-level number.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])
--   True
--   </pre>
data SizeEqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> is non-empty.
type NonEmpty = SizeGreaterThan 0

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> contains elements
--   in a strictly ascending order.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])
--   True
--   </pre>
data Ascending

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> contains elements
--   in a strictly descending order.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])
--   True
--   </pre>
data Descending

-- | A typeclass containing "safe" conversions between refined predicates
--   where the target is <i>weaker</i> 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 <a>weaken</a> is safe to use:
--   
--   <pre>
--   instance <a>Weaken</a> Pred1 Pred2
--   </pre>
--   
--   For most of the instances, explicit type annotations for the result
--   value's type might be required.
class Weaken from to
weaken :: Weaken from to => Refined from x -> Refined to x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken (And l r) l
--   </pre>
andLeft :: Refined (And l r) x -> Refined l x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken (And l r) r
--   </pre>
andRight :: Refined (And l r) x -> Refined r x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken l (Or l r)
--   </pre>
leftOr :: Refined l x -> Refined (Or l r) x

-- | This function helps type inference. It is equivalent to the following:
--   
--   <pre>
--   instance Weaken r (Or l r)
--   </pre>
rightOr :: Refined r x -> Refined (Or l r) x

-- | An exception encoding the way in which a <a>Predicate</a> failed.
data RefineException

-- | A <a>RefineException</a> for failures involving the <a>Not</a>
--   predicate.
RefineNotException :: !TypeRep -> RefineException

-- | A <a>RefineException</a> for failures involving the <a>And</a>
--   predicate.
RefineAndException :: !TypeRep -> !These RefineException RefineException -> RefineException

-- | A <a>RefineException</a> for failures involving the <a>Or</a>
--   predicate.
RefineOrException :: !TypeRep -> !RefineException -> !RefineException -> RefineException

-- | A <a>RefineException</a> for failures involving all other predicates.
RefineOtherException :: !TypeRep -> !Doc Void -> RefineException

-- | Display a <a>RefineException</a> as a <tt><a>Doc</a> ann</tt>
displayRefineException :: RefineException -> Doc ann

-- | A monad transformer that adds <tt><a>RefineException</a></tt>s to
--   other monads.
--   
--   The <tt><a>pure</a></tt> and <tt><a>return</a></tt> functions yield
--   computations that produce the given value, while
--   <tt><tt>&gt;&gt;=</tt></tt> sequences two subcomputations, exiting on
--   the first <tt><a>RefineException</a></tt>.
data RefineT m a

-- | The inverse of <tt><a>RefineT</a></tt>.
runRefineT :: RefineT m a -> m (Either RefineException a)

-- | Map the unwrapped computation using the given function.
--   
--   <pre>
--   <a>runRefineT</a> (<a>mapRefineT</a> f m) = f (<a>runRefineT</a> m)
--   </pre>
mapRefineT :: (m (Either RefineException a) -> n (Either RefineException b)) -> RefineT m a -> RefineT n b

-- | <tt><a>RefineM</a> a</tt> is equivalent to <tt><a>RefineT</a>
--   <a>Identity</a> a</tt> for any type <tt>a</tt>.
type RefineM a = RefineT Identity a

-- | Constructs a computation in the <a>RefineM</a> monad. (The inverse of
--   <tt><a>runRefineM</a></tt>).
refineM :: Either RefineException a -> RefineM a

-- | Run a monadic action of type <tt><a>RefineM</a> a</tt>, yielding an
--   <tt><a>Either</a> <a>RefineException</a> a</tt>.
--   
--   This is just defined as <tt><a>runIdentity</a> <a>.</a>
--   <a>runRefineT</a></tt>.
runRefineM :: RefineM a -> Either RefineException a

-- | One can use <tt><a>throwRefine</a></tt> inside of a monadic context to
--   begin processing a <tt><a>RefineException</a></tt>.
throwRefine :: Monad m => RefineException -> RefineT m a

-- | A handler function to handle previous <tt><a>RefineException</a></tt>s
--   and return to normal execution. A common idiom is:
--   
--   <pre>
--   do { action1; action2; action3 } `<tt>catchRefine'</tt> handler
--   </pre>
--   
--   where the action functions can call <tt><a>throwRefine</a></tt>. 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

-- | A handler for a <tt><a>RefineException</a></tt>.
--   
--   <a>throwRefineOtherException</a> is useful for defining what behaviour
--   <a>validate</a> should have in the event of a predicate failure.
throwRefineOtherException :: Monad m => TypeRep -> Doc Void -> RefineT m a

-- | <pre>
--   &gt;&gt;&gt; pretty 1 &lt;+&gt; pretty "hello" &lt;+&gt; pretty 1.234
--   1 hello 1.234
--   </pre>
pretty :: Pretty a => a -> Doc ann


-- | This module exposes <i>unsafe</i> refinements. An <i>unsafe</i>
--   refinement is one which either does not make the guarantee of totality
--   in construction of the <a>Refined</a> value or does not perform a
--   check of the refinement predicate. It is recommended only to use this
--   when you can manually prove that the refinement predicate holds.
module Refined.Unsafe

-- | A refinement type, which wraps a value of type <tt>x</tt>, ensuring
--   that it satisfies a type-level predicate <tt>p</tt>.
data Refined p x

-- | Constructs a <a>Refined</a> value, completely ignoring any
--   refinements! Use this only when you can manually prove that the
--   refinement holds.
reallyUnsafeRefine :: x -> Refined p x

-- | Constructs a <a>Refined</a> value at run-time, calling <a>error</a> if
--   the value does not satisfy the predicate.
--   
--   WARNING: this function is not total!
unsafeRefine :: Predicate p x => x -> Refined p x

-- | A coercion between a type and any refinement of that type. See
--   <a>Data.Type.Coercion</a> for functions manipulating coercions.
reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x)

-- | Reveal that <tt>x</tt> and <tt><a>Refined</a> p x</tt> are
--   <a>Coercible</a> for <i>all</i> <tt>x</tt> and <tt>p</tt>
--   simultaneously.
--   
--   <h3>Example</h3>
--   
--   <pre>
--   reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)
--   reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion
--   </pre>
reallyUnsafeAllUnderlyingRefined :: (forall x y p. Coercible x y => Coercible y (Refined p x) => r) -> r

-- | A coercion between two <a>Refined</a> types, magicking up the claim
--   that one predicate is entirely equivalent to another.
reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)


-- | This module exports the <a>Refined</a> type with its constructor. This
--   is very risky! In particular, the <tt>Coercible</tt> instances will be
--   visible throughout the importing module. It is usually better to build
--   the necessary coercions locally using the utilities in
--   <a>Refined.Unsafe</a>, but in some cases it may be more convenient to
--   write a separate module that imports this one and exports some large
--   coercion.
module Refined.Unsafe.Type

-- | A refinement type, which wraps a value of type <tt>x</tt>, ensuring
--   that it satisfies a type-level predicate <tt>p</tt>.
newtype Refined p x
Refined :: x -> Refined p x