-- 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


-- | 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>
--   &gt;&gt;&gt; $$(refineTH 23) :: Refined Positive Int
--   Refined 23
--   </pre>
--   
--   Here's an example of an invalid value:
--   
--   <pre>
--   &gt;&gt;&gt; $$(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.
data Not p

-- | The conjunction of two predicates.
data And l r

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

-- | The disjunction of two predicates.
data Or l r

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

-- | A predicate which is satisfied for all types.
data IdPred

-- | A <a>Predicate</a> ensuring that the value is less than the specified
--   type-level number.
data LessThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than the
--   specified type-level number.
data GreaterThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than or equal to
--   the specified type-level number.
data From (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is less than or equal to
--   the specified type-level number.
data To (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is within an inclusive
--   range.
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>.
data EqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is not equal to the
--   specified type-level number <tt>n</tt>.
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 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>.
data NegativeFromTo (n :: Nat) (m :: Nat)

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> has a length
--   which is less than the specified type-level number.
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.
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.
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.
data Ascending

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> contains elements
--   in a strictly descending order.
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 -> 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.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, n GHC.TypeNats.<= m) => Refined.Internal.Predicate (Refined.Internal.NegativeFromTo n m) 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)


-- | 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>
--   &gt;&gt;&gt; $$(refineTH 23) :: Refined Positive Int
--   Refined 23
--   </pre>
--   
--   Here's an example of an invalid value:
--   
--   <pre>
--   &gt;&gt;&gt; $$(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.
data Not p

-- | The conjunction of two predicates.
data And l r

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

-- | The disjunction of two predicates.
data Or l r

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

-- | A predicate which is satisfied for all types.
data IdPred

-- | A <a>Predicate</a> ensuring that the value is less than the specified
--   type-level number.
data LessThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than the
--   specified type-level number.
data GreaterThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is greater than or equal to
--   the specified type-level number.
data From (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is less than or equal to
--   the specified type-level number.
data To (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is within an inclusive
--   range.
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>.
data EqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is not equal to the
--   specified type-level number <tt>n</tt>.
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.
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.
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.
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.
data Ascending

-- | A <a>Predicate</a> ensuring that the <a>Foldable</a> contains elements
--   in a strictly descending order.
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 -> 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 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 <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 <tt>Refined</tt> type.
--   This is unavoidable given the current module structure.
module Refined.Orphan


-- | 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