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


-- | Constraint manipulation
--   
--   GHC 7.4 gave us the ability to talk about <tt>ConstraintKinds</tt>.
--   They stopped crashing the compiler in GHC 7.6.
--   
--   This package provides a vocabulary for working with them.
@package constraints
@version 0.4.1.3


-- | <tt>ConstraintKinds</tt> made type classes into types of a new kind,
--   <tt>Constraint</tt>.
--   
--   <pre>
--   <a>Eq</a> :: * -&gt; <a>Constraint</a>
--   <a>Ord</a> :: * -&gt; <a>Constraint</a>
--   <a>Monad</a> :: (* -&gt; *) -&gt; <a>Constraint</a>
--   </pre>
--   
--   The need for this extension was first publicized in the paper
--   
--   <a>Scrap your boilerplate with class: extensible generic functions</a>
--   
--   by Ralf Lämmel and Simon Peyton Jones in 2005, which shoehorned all
--   the things they needed into a custom <tt>Sat</tt> typeclass.
--   
--   With <tt>ConstraintKinds</tt> we can put into code a lot of tools for
--   manipulating these new types without such awkward workarounds.
module Data.Constraint
data Constraint :: BOX

-- | Values of type <tt><a>Dict</a> p</tt> capture a dictionary for a
--   constraint of type <tt>p</tt>.
--   
--   e.g.
--   
--   <pre>
--   <a>Dict</a> :: <a>Dict</a> (<a>Eq</a> <a>Int</a>)
--   </pre>
--   
--   captures a dictionary that proves we have an:
--   
--   <pre>
--   instance <a>Eq</a> 'Int
--   </pre>
--   
--   Pattern matching on the <a>Dict</a> constructor will bring this
--   instance into scope.
data Dict :: Constraint -> *
Dict :: Dict a

-- | This is the type of entailment.
--   
--   <tt>a <a>:-</a> b</tt> is read as <tt>a</tt> "entails" <tt>b</tt>.
--   
--   With this we can actually build a category for <a>Constraint</a>
--   resolution.
--   
--   e.g.
--   
--   Because <tt><a>Eq</a> a</tt> is a superclass of <tt><a>Ord</a> a</tt>,
--   we can show that <tt><a>Ord</a> a</tt> entails <tt><a>Eq</a> a</tt>.
--   
--   Because <tt>instance <a>Ord</a> a =&gt; <a>Ord</a> [a]</tt> exists, we
--   can show that <tt><a>Ord</a> a</tt> entails <tt><a>Ord</a> [a]</tt> as
--   well.
--   
--   This relationship is captured in the <a>:-</a> entailment type here.
--   
--   Since <tt>p <a>:-</a> p</tt> and entailment composes, <a>:-</a> forms
--   the arrows of a <a>Category</a> of constraints. However,
--   <a>Category</a> only because sufficiently general to support this
--   instance in GHC 7.8, so prior to 7.8 this instance is unavailable.
--   
--   But due to the coherence of instance resolution in Haskell, this
--   <a>Category</a> has some very interesting properties. Notably, in the
--   absence of <tt>IncoherentInstances</tt>, this category is "thin",
--   which is to say that between any two objects (constraints) there is at
--   most one distinguishable arrow.
--   
--   This means that for instance, even though there are two ways to derive
--   <tt><a>Ord</a> a <a>:-</a> <a>Eq</a> [a]</tt>, the answers from these
--   two paths _must_ by construction be equal. This is a property that
--   Haskell offers that is pretty much unique in the space of languages
--   with things they call "type classes".
--   
--   What are the two ways?
--   
--   Well, we can go from <tt><a>Ord</a> a <a>:-</a> <a>Eq</a> a</tt> via
--   the superclass relationship, and them from <tt><a>Eq</a> a <a>:-</a>
--   <a>Eq</a> [a]</tt> via the instance, or we can go from <tt><a>Ord</a>
--   a <a>:-</a> <a>Ord</a> [a]</tt> via the instance then from
--   <tt><a>Ord</a> [a] <a>:-</a> <a>Eq</a> [a]</tt> through the superclass
--   relationship and this diagram by definition must "commute".
--   
--   Diagrammatically,
--   
--   <pre>
--          Ord a
--      ins /     \ cls
--         v       v
--   Ord [a]     Eq a
--      cls \     / ins
--           v   v
--          Eq [a]
--   </pre>
--   
--   This safety net ensures that pretty much anything you can write with
--   this library is sensible and can't break any assumptions on the behalf
--   of library authors.
newtype (:-) a b
Sub :: (a => Dict b) -> (:-) a b

-- | Given that <tt>a :- b</tt>, derive something that needs a context
--   <tt>b</tt>, using the context <tt>a</tt>
(\\) :: a => (b => r) -> (a :- b) -> r

-- | Weakening a constraint product
--   
--   The category of constraints is Cartesian. We can forget information.
weaken1 :: (a, b) :- a

-- | Weakening a constraint product
--   
--   The category of constraints is Cartesian. We can forget information.
weaken2 :: (a, b) :- b

-- | Contracting a constraint / diagonal morphism
--   
--   The category of constraints is Cartesian. We can reuse information.
contract :: a :- (a, a)

-- | Constraint product
--   
--   <pre>
--   trans weaken1 (f &amp;&amp;&amp; g) = f
--   trans weaken2 (f &amp;&amp;&amp; g) = g
--   </pre>
(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c)

-- | due to the hack for the kind of <tt>(,)</tt> in the current version of
--   GHC we can't actually make instances for <tt>(,) :: Constraint -&gt;
--   Constraint -&gt; Constraint</tt>, but <tt>(,)</tt> is a bifunctor on
--   the category of constraints. This lets us map over both sides.
(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)

-- | Transitivity of entailment
--   
--   If we view <tt>(<a>:-</a>)</tt> as a Constraint-indexed category, then
--   this is <tt>(<a>.</a>)</tt>
trans :: (b :- c) -> (a :- b) -> a :- c

-- | Reflexivity of entailment
--   
--   If we view <tt>(<a>:-</a>)</tt> as a Constraint-indexed category, then
--   this is <a>id</a>
refl :: a :- a

-- | Every constraint implies truth
--   
--   These are the terminal arrows of the category, and <tt>()</tt> is the
--   terminal object.
--   
--   Given any constraint there is a unique entailment of the <tt>()</tt>
--   constraint from that constraint.
top :: a :- ()

-- | A bad type coercion lets you derive any constraint you want.
--   
--   These are the initial arrows of the category and <tt>(() ~ Bool)</tt>
--   is the initial object
--   
--   This demonstrates the law of classical logic <a>"ex falso
--   quodlibet"</a>
bottom :: (() ~ Bool) :- c

-- | Apply an entailment to a dictionary.
--   
--   From a category theoretic perspective <a>Dict</a> is a functor that
--   maps from the category of constraints (with arrows in <a>:-</a>) to
--   the category Hask of Haskell data types.
mapDict :: (a :- b) -> Dict a -> Dict b

-- | This functor is fully faithful, which is to say that given any
--   function you can write <tt>Dict a -&gt; Dict b</tt> there also exists
--   an entailment <tt>a :- b</tt> in the category of constraints that you
--   can build.
unmapDict :: (Dict a -> Dict b) -> a :- b

-- | Reify the relationship between a class and its superclass constraints
--   as a class
--   
--   Given a definition such as
--   
--   <pre>
--   class Foo a =&gt; Bar a
--   </pre>
--   
--   you can capture the relationship between 'Bar a' and its superclass
--   'Foo a' with
--   
--   <pre>
--   instance <a>Class</a> (Foo a) (Bar a) where <a>cls</a> = <a>Sub</a> <a>Dict</a>
--   </pre>
--   
--   Now the user can use 'cls :: Bar a :- Foo a'
class Class b h | h -> b
cls :: Class b h => h :- b

-- | Reify the relationship between an instance head and its body as a
--   class
--   
--   Given a definition such as
--   
--   <pre>
--   instance Foo a =&gt; Foo [a]
--   </pre>
--   
--   you can capture the relationship between the instance head and its
--   body with
--   
--   <pre>
--   instance Foo a <a>:=&gt;</a> Foo [a] where <a>ins</a> = <a>Sub</a> <a>Dict</a>
--   </pre>
class (:=>) b h | h -> b
ins :: (:=>) b h => b :- h
instance Typeable Dict
instance Typeable (:-)
instance (a) => Read (Dict a)
instance Show (Dict a)
instance Ord (Dict a)
instance Eq (Dict a)
instance (a) => Monoid (Dict a)
instance a :=> Monoid (Dict a)
instance a :=> Read (Dict a)
instance (a) => Bounded (Dict a)
instance a :=> Bounded (Dict a)
instance (a) => Enum (Dict a)
instance a :=> Enum (Dict a)
instance () :=> MonadPlus Maybe
instance () :=> MonadPlus []
instance Class (Monad f) (MonadPlus f)
instance () :=> Monad IO
instance () :=> Monad (Either a)
instance () :=> Monad ((->) a)
instance () :=> Monad []
instance Class () (Monad f)
instance MonadPlus m :=> Alternative (WrappedMonad m)
instance () :=> Alternative Maybe
instance () :=> Alternative []
instance Class (Applicative f) (Alternative f)
instance Monad m :=> Applicative (WrappedMonad m)
instance Monoid a :=> Applicative ((,) a)
instance () :=> Applicative IO
instance () :=> Applicative ((->) a)
instance () :=> Applicative (Either a)
instance () :=> Applicative Maybe
instance () :=> Applicative []
instance Class (Functor f) (Applicative f)
instance Monad m :=> Functor (WrappedMonad m)
instance () :=> Functor IO
instance () :=> Functor ((,) a)
instance () :=> Functor ((->) a)
instance () :=> Functor (Either a)
instance () :=> Functor Maybe
instance () :=> Functor []
instance Class () (Functor f)
instance (Monoid a, Monoid b) :=> Monoid (a, b)
instance Monoid a :=> Monoid (Maybe a)
instance () :=> Monoid [a]
instance () :=> Monoid Ordering
instance () :=> Monoid ()
instance Class () (Monoid a)
instance () :=> RealFloat Double
instance () :=> RealFloat Float
instance Class (RealFrac a, Floating a) (RealFloat a)
instance Integral a :=> RealFrac (Ratio a)
instance () :=> RealFrac Double
instance () :=> RealFrac Float
instance Class (Real a, Fractional a) (RealFrac a)
instance RealFloat a :=> Floating (Complex a)
instance () :=> Floating Double
instance () :=> Floating Float
instance Class (Fractional a) (Floating a)
instance Integral a :=> Fractional (Ratio a)
instance RealFloat a :=> Fractional (Complex a)
instance () :=> Fractional Double
instance () :=> Fractional Float
instance Class (Num a) (Fractional a)
instance () :=> Integral Integer
instance () :=> Integral Int
instance Class (Real a, Enum a) (Integral a)
instance Integral a :=> Real (Ratio a)
instance () :=> Real Double
instance () :=> Real Float
instance () :=> Real Integer
instance () :=> Real Int
instance Class (Num a, Ord a) (Real a)
instance Integral a :=> Num (Ratio a)
instance RealFloat a :=> Num (Complex a)
instance () :=> Num Double
instance () :=> Num Float
instance () :=> Num Integer
instance () :=> Num Int
instance Class () (Num a)
instance (Bounded a, Bounded b) :=> Bounded (a, b)
instance () :=> Bounded Char
instance () :=> Bounded Int
instance () :=> Bounded Bool
instance () :=> Bounded Ordering
instance () :=> Bounded ()
instance Class () (Bounded a)
instance Integral a :=> Enum (Ratio a)
instance () :=> Enum Double
instance () :=> Enum Float
instance () :=> Enum Integer
instance () :=> Enum Int
instance () :=> Enum Char
instance () :=> Enum Ordering
instance () :=> Enum Bool
instance () :=> Enum ()
instance Class () (Enum a)
instance (Integral a, Read a) :=> Read (Ratio a)
instance (Read a, Read b) :=> Read (Either a b)
instance (Read a, Read b) :=> Read (a, b)
instance Read a :=> Read (Maybe a)
instance Read a :=> Read [a]
instance Read a :=> Read (Complex a)
instance () :=> Read Char
instance () :=> Read Ordering
instance () :=> Read Bool
instance () :=> Read ()
instance Class () (Read a)
instance () :=> Show (a :- b)
instance () :=> Show (Dict a)
instance (Integral a, Show a) :=> Show (Ratio a)
instance (Show a, Show b) :=> Show (Either a b)
instance (Show a, Show b) :=> Show (a, b)
instance Show a :=> Show (Maybe a)
instance Show a :=> Show [a]
instance Show a :=> Show (Complex a)
instance () :=> Show Char
instance () :=> Show Ordering
instance () :=> Show Bool
instance () :=> Show ()
instance Class () (Show a)
instance () :=> Ord (a :- b)
instance () :=> Ord (Dict a)
instance Integral a :=> Ord (Ratio a)
instance (Ord a, Ord b) :=> Ord (Either a b)
instance (Ord a, Ord b) :=> Ord (a, b)
instance Ord a :=> Ord [a]
instance Ord a :=> Ord (Maybe a)
instance () :=> Ord Char
instance () :=> Ord Double
instance () :=> Ord Float
instance () :=> Ord Integer
instance () :=> Ord Int
instance () :=> Ord Bool
instance () :=> Ord ()
instance Class (Eq a) (Ord a)
instance () :=> Eq (a :- b)
instance () :=> Eq (Dict a)
instance (Eq a, Eq b) :=> Eq (Either a b)
instance (Eq a, Eq b) :=> Eq (a, b)
instance Eq a :=> Eq (Ratio a)
instance Eq a :=> Eq (Complex a)
instance Eq a :=> Eq (Maybe a)
instance Eq a :=> Eq [a]
instance () :=> Eq Double
instance () :=> Eq Float
instance () :=> Eq Integer
instance () :=> Eq Bool
instance () :=> Eq Int
instance () :=> Eq ()
instance Class () (Eq a)
instance () :=> ()
instance Class () ()
instance b :=> a => () :=> (b :=> a)
instance Class b a => () :=> Class b a
instance Class () (b :=> a)
instance Class () (Class b a)
instance Show (a :- b)
instance Ord (a :- b)
instance Eq (a :- b)
instance Category (:-)
instance (Typeable p, Typeable q, p, q) => Data (p :- q)
instance (Typeable p, p) => Data (Dict p)


module Data.Constraint.Unsafe

-- | Coerce a dictionary unsafely from one type to another
unsafeCoerceConstraint :: a :- b

-- | Coerce a dictionary unsafely from one type to a newtype of that type
unsafeDerive :: Newtype n o => (o -> n) -> t o :- t n

-- | Coerce a dictionary unsafely from a newtype of a type to the base type
unsafeUnderive :: Newtype n o => (o -> n) -> t n :- t o

-- | Construct an Applicative instance from a Monad
unsafeApplicative :: Monad m => (Applicative m => m a) -> m a

-- | Construct an Alternative instance from a MonadPlus
unsafeAlternative :: MonadPlus m => (Alternative m => m a) -> m a


-- | This module uses a trick to provide quantification over constraints.
module Data.Constraint.Forall

-- | A quantified constraint
type Forall (p :: * -> Constraint) = (p A, p B)

-- | instantiate a quantified constraint on kind <tt>*</tt>
inst :: Forall p :- p a
type ForallF (p :: * -> Constraint) (f :: * -> *) = (p (f A), p (f B))
instF :: ForallF p f :- p (f a)
type Forall1 (p :: (* -> *) -> Constraint) = (p F, p M)

-- | instantiate a quantified constraint on kind <tt>* -&gt; *</tt>
inst1 :: Forall1 p :- p f
type ForallT (p :: * -> Constraint) (t :: (* -> *) -> * -> *) = (p (t F A), p (t M B))
instT :: ForallT p t :- p (t f a)
