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


-- | This module exports the <a>Refined</a> type with its constructor. This
--   is very risky! In particular, the <a>Coercible</a> 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>.
newtype Refined (p :: k) x

Refined :: x -> Refined (p :: k) x
instance forall k (p :: k). Data.Foldable.Foldable (Refined.Unsafe.Type.Refined p)
instance forall k (p :: k) x. GHC.Show.Show x => GHC.Show.Show (Refined.Unsafe.Type.Refined p x)
instance forall k (p :: k) x. Control.DeepSeq.NFData x => Control.DeepSeq.NFData (Refined.Unsafe.Type.Refined p x)
instance forall k (p :: k) x. Data.Hashable.Class.Hashable x => Data.Hashable.Class.Hashable (Refined.Unsafe.Type.Refined p x)
instance forall k (p :: k) x. GHC.Classes.Ord x => GHC.Classes.Ord (Refined.Unsafe.Type.Refined p x)
instance forall k (p :: k) x. GHC.Classes.Eq x => GHC.Classes.Eq (Refined.Unsafe.Type.Refined p x)
instance forall k x (p :: k). Language.Haskell.TH.Syntax.Lift x => Language.Haskell.TH.Syntax.Lift (Refined.Unsafe.Type.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>
module Refined

-- | A refinement type, which wraps a value of type <tt>x</tt>.
data Refined (p :: k) x

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

-- | Like <a>refine</a>, but discards the refinement. This _can_ be useful
--   when you only need to validate that some value at runtime satisfies
--   some predicate. See also <a>reifyPredicate</a>.
refine_ :: forall p x. Predicate p x => x -> Either RefineException 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)

-- | Like <a>refine</a>, but, when the value doesn't satisfy the predicate,
--   returns a <a>Refined</a> value with the predicate negated, instead of
--   returning <a>RefineException</a>.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refineEither @Even @Int 42)
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refineEither @Even @Int 43)
--   True
--   </pre>
refineEither :: forall p x. Predicate p x => x -> Either (Refined (Not p) x) (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>
--   
--   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.
--   
--   <i>Note</i>: It may be useful to use this function with the
--   <a>th-lift-instances package</a>.
refineTH :: forall p x m. (Predicate p x, Lift x, Quote m, MonadFail m) => x -> Code m (Refined p x)

-- | Like <a>refineTH</a>, but immediately unrefines the value. This is
--   useful when some value need only be refined at compile-time.
refineTH_ :: forall p x m. (Predicate p x, Lift x, Quote m, MonadFail m) => x -> Code m 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 <a>RefineException</a> if the value does not
--   satisfy.
--   
--   <i>Note</i>: <a>validate</a> 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 <a>Maybe</a> here should
--   be interpreted to mean the presence or absence of a
--   <a>RefineException</a>, and nothing else.
validate :: Predicate p x => Proxy p -> x -> Maybe RefineException

-- | Reify a <a>Predicate</a> by turning it into a value-level predicate.
reifyPredicate :: forall p a. Predicate p a => a -> Bool

-- | 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>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(Or Even Even) @Int 4)
--   True
--   </pre>
data Or l r

Or :: Or l r

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

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

Xor :: Xor l r

-- | A predicate which is satisfied for all types. Arguments passed to
--   <tt><a>validate</a></tt> in <tt><a>validate</a> <a>IdPred</a> x</tt>
--   are not evaluated.
--   
--   <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 (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)

GreaterThan :: 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)

From :: 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)

To :: 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)

FromTo :: FromTo (mn :: Nat) (mx :: Nat)

-- | 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 (n :: Nat) (m :: 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)

EqualTo :: 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)

NotEqualTo :: NotEqualTo (n :: Nat)

-- | 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>.
--   
--   <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 (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value is IEEE "not-a-number"
--   (NaN).
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @NaN @Double (0/0))
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @NaN @Double 13.9)
--   True
--   </pre>
data NaN

NaN :: NaN

-- | A <a>Predicate</a> ensuring that the value is IEEE infinity or
--   negative infinity.
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @Infinite @Double (1/0))
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @Infinite @Double (-1/0))
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @Infinite @Double 13.20)
--   True
--   </pre>
data Infinite

Infinite :: Infinite

-- | 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 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>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeLessThan 4) @Text "Hi")
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(SizeLessThan 4) @Text "Hello")
--   True
--   </pre>
data SizeLessThan (n :: Nat)

SizeLessThan :: SizeLessThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value 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>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(SizeGreaterThan 4) @Text "Hi")
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeGreaterThan 4) @Text "Hello")
--   True
--   </pre>
data SizeGreaterThan (n :: Nat)

SizeGreaterThan :: SizeGreaterThan (n :: Nat)

-- | A <a>Predicate</a> ensuring that the value 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>
--   
--   <pre>
--   &gt;&gt;&gt; isRight (refine @(SizeEqualTo 4) @Text "four")
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isLeft (refine @(SizeEqualTo 35) @Text "four")
--   True
--   </pre>
data SizeEqualTo (n :: Nat)

SizeEqualTo :: SizeEqualTo (n :: Nat)

-- | A <a>Predicate</a> ensuring that the type is empty.
type Empty = SizeEqualTo 0

-- | A <a>Predicate</a> ensuring that the type 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 guaranteed to satisfy 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

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

-- | 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 the <a>Xor</a>
--   predicate.
RefineXorException :: !TypeRep -> !Maybe (RefineException, RefineException) -> RefineException

-- | A <a>RefineException</a> for failures involving all other predicates
--   with custom exception.
RefineSomeException :: !TypeRep -> !SomeException -> RefineException

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

-- | Display a <a>RefineException</a> as <tt><a>String</a></tt>
--   
--   This function can be extremely useful for debugging
--   <tt><a>RefineException</a>s</tt>, especially deeply nested ones.
--   
--   Consider:
--   
--   <pre>
--   myRefinement = refine
--     @(And
--         (Not (LessThan 5))
--         (Xor
--           (DivisibleBy 10)
--           (And
--             (EqualTo 4)
--             (EqualTo 3)
--           )
--         )
--      )
--     @Int
--     3
--   
--   </pre>
--   
--   This function will show the following tree structure, recursively
--   breaking down every issue:
--   
--   <pre>
--   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
--   
--   </pre>
--   
--   <i>Note</i>: Equivalent to <tt><a>show</a>
--   @<a>RefineException</a></tt>
displayRefineException :: RefineException -> String

-- | 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.
--   
--   Typically the first argument passed to this function will be the
--   result of applying <a>typeRep</a> to the first argument of
--   <a>validate</a>.
throwRefineOtherException :: TypeRep -> Text -> Maybe RefineException

-- | A handler for a <tt><a>RefineException</a></tt>.
--   
--   <a>throwRefineSomeException</a> is useful for defining what behaviour
--   <a>validate</a> should have in the event of a predicate failure with a
--   specific exception.
throwRefineSomeException :: TypeRep -> SomeException -> Maybe RefineException

-- | An implementation of <a>validate</a> that always succeeds.
--   
--   <h4><b>Examples</b></h4>
--   
--   <pre>
--   data ContainsLetterE = ContainsLetterE
--   
--   instance Predicate ContainsLetterE <a>Text</a> where
--     validate p t
--       | <a>any</a> (== 'e') t = <a>success</a>
--       | otherwise = Just $ <tt>throwRefineException</tt> (typeRep p) "Text doesn't contain letter 'e'".
--   
--   </pre>
success :: Maybe RefineException
instance GHC.Generics.Generic Refined.IdPred
instance GHC.Generics.Generic1 Refined.Not
instance forall k (p :: k). GHC.Generics.Generic (Refined.Not p)
instance forall k1 k2 (l :: k2). GHC.Generics.Generic1 (Refined.And l)
instance forall k1 (l :: k1) k2 (r :: k2). GHC.Generics.Generic (Refined.And l r)
instance forall k1 k2 (l :: k2). GHC.Generics.Generic1 (Refined.Or l)
instance forall k1 (l :: k1) k2 (r :: k2). GHC.Generics.Generic (Refined.Or l r)
instance forall k1 k2 (l :: k2). GHC.Generics.Generic1 (Refined.Xor l)
instance forall k1 (l :: k1) k2 (r :: k2). GHC.Generics.Generic (Refined.Xor l r)
instance GHC.Generics.Generic (Refined.SizeLessThan n)
instance GHC.Generics.Generic (Refined.SizeGreaterThan n)
instance GHC.Generics.Generic (Refined.SizeEqualTo n)
instance GHC.Generics.Generic Refined.Ascending
instance GHC.Generics.Generic Refined.Descending
instance GHC.Generics.Generic (Refined.LessThan n)
instance GHC.Generics.Generic (Refined.GreaterThan n)
instance GHC.Generics.Generic (Refined.From n)
instance GHC.Generics.Generic (Refined.To n)
instance GHC.Generics.Generic (Refined.FromTo mn mx)
instance GHC.Generics.Generic (Refined.EqualTo n)
instance GHC.Generics.Generic (Refined.NotEqualTo n)
instance GHC.Generics.Generic (Refined.NegativeFromTo n m)
instance GHC.Generics.Generic (Refined.DivisibleBy n)
instance GHC.Generics.Generic Refined.Odd
instance GHC.Generics.Generic Refined.NaN
instance GHC.Generics.Generic Refined.Infinite
instance GHC.Generics.Generic Refined.Even
instance GHC.Generics.Generic Refined.RefineException
instance forall k x (p :: k). (GHC.Read.Read x, Refined.Predicate p x) => GHC.Read.Read (Refined.Unsafe.Type.Refined p x)
instance forall k a (p :: k). (Data.Aeson.Types.FromJSON.FromJSON a, Refined.Predicate p a) => Data.Aeson.Types.FromJSON.FromJSON (Refined.Unsafe.Type.Refined p a)
instance forall k a (p :: k). (Data.Aeson.Types.FromJSON.FromJSONKey a, Refined.Predicate p a) => Data.Aeson.Types.FromJSON.FromJSONKey (Refined.Unsafe.Type.Refined p a)
instance forall k a (p :: k). (Data.Aeson.Types.ToJSON.ToJSON a, Refined.Predicate p a) => Data.Aeson.Types.ToJSON.ToJSON (Refined.Unsafe.Type.Refined p a)
instance forall k a (p :: k). (Data.Aeson.Types.ToJSON.ToJSONKey a, Refined.Predicate p a) => Data.Aeson.Types.ToJSON.ToJSONKey (Refined.Unsafe.Type.Refined p a)
instance forall k (p :: k) a. (Test.QuickCheck.Arbitrary.Arbitrary a, Data.Typeable.Internal.Typeable a, Data.Typeable.Internal.Typeable p, Refined.Predicate p a) => Test.QuickCheck.Arbitrary.Arbitrary (Refined.Unsafe.Type.Refined p a)
instance Refined.Predicate Refined.IdPred x
instance forall k (p :: k) x. (Refined.Predicate p x, Data.Typeable.Internal.Typeable p, Data.Typeable.Internal.Typeable k) => Refined.Predicate (Refined.Not p) x
instance forall k (l :: k) x (r :: k). (Refined.Predicate l x, Refined.Predicate r x, Data.Typeable.Internal.Typeable l, Data.Typeable.Internal.Typeable r, Data.Typeable.Internal.Typeable k) => Refined.Predicate (Refined.And l r) x
instance forall k (l :: k) x (r :: k). (Refined.Predicate l x, Refined.Predicate r x, Data.Typeable.Internal.Typeable l, Data.Typeable.Internal.Typeable r, Data.Typeable.Internal.Typeable k) => Refined.Predicate (Refined.Or l r) x
instance forall k (l :: k) x (r :: k). (Refined.Predicate l x, Refined.Predicate r x, Data.Typeable.Internal.Typeable l, Data.Typeable.Internal.Typeable r, Data.Typeable.Internal.Typeable k) => Refined.Predicate (Refined.Xor l r) x
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.SizeLessThan n) (t a)
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeLessThan n) Data.Text.Internal.Text
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeLessThan n) Data.ByteString.Internal.ByteString
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeLessThan n) Data.ByteString.Lazy.Internal.ByteString
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.SizeGreaterThan n) (t a)
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeGreaterThan n) Data.Text.Internal.Text
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeGreaterThan n) Data.ByteString.Internal.ByteString
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeGreaterThan n) Data.ByteString.Lazy.Internal.ByteString
instance (Data.Foldable.Foldable t, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.SizeEqualTo n) (t a)
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeEqualTo n) Data.Text.Internal.Text
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeEqualTo n) Data.ByteString.Internal.ByteString
instance GHC.TypeNats.KnownNat n => Refined.Predicate (Refined.SizeEqualTo n) Data.ByteString.Lazy.Internal.ByteString
instance (Data.Foldable.Foldable t, GHC.Classes.Ord a) => Refined.Predicate Refined.Ascending (t a)
instance (Data.Foldable.Foldable t, GHC.Classes.Ord a) => Refined.Predicate Refined.Descending (t a)
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.LessThan n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.GreaterThan n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.From n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.To n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat mn, GHC.TypeNats.KnownNat mx, mn Data.Type.Ord.<= mx) => Refined.Predicate (Refined.FromTo mn mx) x
instance (GHC.Classes.Eq x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.EqualTo n) x
instance (GHC.Classes.Eq x, GHC.Num.Num x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.NotEqualTo n) x
instance (GHC.Classes.Ord x, GHC.Num.Num x, GHC.TypeNats.KnownNat n, GHC.TypeNats.KnownNat m) => Refined.Predicate (Refined.NegativeFromTo n m) x
instance (GHC.Real.Integral x, GHC.TypeNats.KnownNat n) => Refined.Predicate (Refined.DivisibleBy n) x
instance GHC.Real.Integral x => Refined.Predicate Refined.Odd x
instance GHC.Float.RealFloat x => Refined.Predicate Refined.NaN x
instance GHC.Float.RealFloat x => Refined.Predicate Refined.Infinite x
instance GHC.Real.Integral x => Refined.Predicate Refined.Even x
instance GHC.Show.Show Refined.RefineException
instance GHC.Exception.Type.Exception Refined.RefineException
instance (n Data.Type.Ord.<= m) => Refined.Weaken (Refined.LessThan n) (Refined.LessThan m)
instance (n Data.Type.Ord.<= m) => Refined.Weaken (Refined.LessThan n) (Refined.To m)
instance (n Data.Type.Ord.<= m) => Refined.Weaken (Refined.To n) (Refined.To m)
instance (m Data.Type.Ord.<= n) => Refined.Weaken (Refined.GreaterThan n) (Refined.GreaterThan m)
instance (m Data.Type.Ord.<= n) => Refined.Weaken (Refined.GreaterThan n) (Refined.From m)
instance (m Data.Type.Ord.<= n) => Refined.Weaken (Refined.From n) (Refined.From m)
instance (p Data.Type.Ord.<= n, m Data.Type.Ord.<= q) => Refined.Weaken (Refined.FromTo n m) (Refined.FromTo p q)
instance (p Data.Type.Ord.<= n) => Refined.Weaken (Refined.FromTo n m) (Refined.From p)
instance (m Data.Type.Ord.<= q) => Refined.Weaken (Refined.FromTo n m) (Refined.To q)


-- | 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>.
data Refined (p :: k) 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)