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


-- | Combinators for manipulating dependently-typed predicates.
--   
--   This library provides combinators and typeclasses for working and
--   manipulating type-level predicates in Haskell, which are represented
--   as matchable type-level functions <tt>k ~&gt; Type</tt> from the
--   <tt>singletons</tt> library. See <a>Data.Type.Predicate</a> for a good
--   starting point, and the documentation for <a>Predicate</a> on how to
--   define predicates.
@package decidable
@version 0.3.1.1


-- | Combinators for working with type-level predicates, along with
--   typeclasses for canonical proofs and deciding functions.
module Data.Type.Predicate

-- | A type-level predicate in Haskell. We say that the predicate <tt>P ::
--   <a>Predicate</a> k</tt> is true/satisfied by input <tt>x :: k</tt> if
--   there exists a value of type <tt>P @@ x</tt>, and that it
--   false/disproved if such a value cannot exist. (Where <a>@@</a> is
--   <a>Apply</a>, the singleton library's type-level function application
--   for mathcable functions). In some contexts, this is also known as a
--   dependently typed "view".
--   
--   See <a>Provable</a> and <a>Decidable</a> for more information on how
--   to use, prove and decide these predicates.
--   
--   The kind <tt>k ~&gt; <a>Type</a></tt> is the kind of "matchable"
--   type-level functions in Haskell. They are type-level functions that
--   are encoded as dummy type constructors ("defunctionalization symbols")
--   that can be decidedly "matched" on for things like typeclass
--   instances.
--   
--   There are two ways to define your own predicates:
--   
--   <ol>
--   <li>Using the predicate combinators and predicate transformers in this
--   library and the <i>singletons</i> library, which let you construct
--   pre-made predicates and sometimes create predicates from other
--   predicates.</li>
--   <li>Manually creating a data type that acts as a matchable
--   predicate.</li>
--   </ol>
--   
--   For an example of the latter, we can create the "not p" predicate,
--   which takes a predicate <tt>p</tt> as input and returns the negation
--   of the predicate:
--   
--   <pre>
--   -- First, create the data type with the kind signature you want
--   data Not :: Predicate k -&gt; Predicate k
--   
--   -- Then, write the <a>Apply</a> instance, to specify the type of the
--   -- witnesses of that predicate
--   instance <a>Apply</a> (Not p) a = (p <a>@@</a> a) -&gt; <a>Void</a>
--   </pre>
--   
--   See the source of <a>Data.Type.Predicate</a> and
--   <a>Data.Type.Predicate.Logic</a> for simple examples of hand-made
--   predicates. For example, we have the always-true predicate
--   <a>Evident</a>:
--   
--   <pre>
--   data Evident :: <a>Predicate</a> k
--   instance Apply Evident a = <a>Sing</a> a
--   </pre>
--   
--   And the "and" predicate combinator:
--   
--   <pre>
--   data (&amp;&amp;&amp;) :: Predicate k -&gt; Predicate k -&gt; Predicate k
--   instance Apply (p &amp;&amp;&amp; q) a = (p <a>@@</a> a, q <a>@@</a> a)
--   </pre>
--   
--   Typically it is recommended to create predicates from the supplied
--   predicate combinators (<a>TyPred</a> can be used for any type
--   constructor to turn it into a predicate, for instance) whenever
--   possible.
type Predicate k = k ~> Type

-- | A <tt><a>Wit</a> p a</tt> is a value of type <tt>p @@ a</tt> --- that
--   is, it is a proof or witness that <tt>p</tt> is satisfied for
--   <tt>a</tt>.
--   
--   It essentially turns a <tt>k ~&gt; <a>Type</a></tt> ("matchable"
--   <tt><a>Predicate</a> k</tt>) /back into/ a <tt>k -&gt;
--   <a>Type</a></tt> predicate.
newtype Wit p a
Wit :: (p @@ a) -> Wit p a
[getWit] :: Wit p a -> p @@ a

-- | Convert a normal <tt>-&gt;</tt> type constructor into a
--   <a>Predicate</a>.
--   
--   <pre>
--   <a>TyPred</a> :: (k -&gt; <a>Type</a>) -&gt; <a>Predicate</a> k
--   </pre>
type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)

-- | The always-true predicate.
--   
--   <pre>
--   <a>Evident</a> :: <a>Predicate</a> k
--   </pre>
data Evident :: Predicate k

-- | <tt><a>EqualTo</a> a</tt> is a predicate that the input is equal to
--   <tt>a</tt>.
--   
--   <pre>
--   <a>EqualTo</a> :: k -&gt; <a>Predicate</a> k
--   </pre>
type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)

-- | Convert a tradtional <tt>k ~&gt; <a>Bool</a></tt> predicate into a
--   <a>Predicate</a>.
--   
--   <pre>
--   <a>BoolPred</a> :: (k ~&gt; Bool) -&gt; Predicate k
--   </pre>
type BoolPred (p :: k ~> Bool) = (PMap p (EqualTo 'True) :: Predicate k)

-- | The always-false predicate
--   
--   Could also be defined as <tt><a>ConstSym1</a> Void</tt>, but this
--   defintion gives us a free <a>Decidable</a> instance.
--   
--   <pre>
--   <a>Impossible</a> :: <a>Predicate</a> k
--   </pre>
type Impossible = (Not Evident :: Predicate k)

-- | <tt><a>In</a> f as</tt> is a predicate that a given input <tt>a</tt>
--   is a member of collection <tt>as</tt>.
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as

-- | Pre-compose a function to a predicate
--   
--   <pre>
--   <a>PMap</a> :: (k ~&gt; j) -&gt; <a>Predicate</a> j -&gt; Predicate k
--   </pre>
type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)

-- | <tt><a>Not</a> p</tt> is the predicate that <tt>p</tt> is not true.
data Not :: Predicate k -> Predicate k

-- | Decide <tt><a>Not</a> p</tt> based on decisions of <tt>p</tt>.
decideNot :: forall p a. () => Decision (p @@ a) -> Decision (Not p @@ a)

-- | A proving function for predicate <tt>p</tt>; in some contexts, also
--   called a "view function". See <a>Provable</a> for more information.
type Prove p = forall a. Sing a -> p @@ a

-- | We say that <tt>p</tt> implies <tt>q</tt> (<tt>p <a>--&gt;</a> q</tt>)
--   if, given <tt>p </tt><tt> a</tt>, we can always prove <tt>q @@ a</tt>.
type p --> q = forall a. Sing a -> p @@ a -> q @@ a
infixr 1 -->

-- | This is implication <a>--&gt;#</a>, but only in a specific context
--   <tt>h</tt>.
type ( p --># q ) h = forall a. Sing a -> p @@ a -> h (q @@ a)
infixr 1 -->#

-- | A typeclass for provable predicates (constructivist tautologies). In
--   some context, these are also known as "views".
--   
--   A predicate is provable if, given any input <tt>a</tt>, you can
--   generate a proof of <tt>p @@ a</tt>. Essentially, it means that a
--   predicate is "always true".
--   
--   We can call a type a view if, for any input <tt>a</tt>, there is
--   <i>some</i> constructor of <tt>p @@ a</tt> that can we can use to
--   "categorize" <tt>a</tt>.
--   
--   This typeclass associates a canonical proof function for every
--   provable predicate, or a canonical view function for any view.
--   
--   It confers two main advatnages:
--   
--   <ol>
--   <li>The proof function<i>view for every predicate</i>view is available
--   via the same name</li>
--   <li>We can write <a>Provable</a> instances for polymorphic predicate
--   transformers (predicates parameterized on other predicates) easily, by
--   refering to <a>Provable</a> instances of the transformed
--   predicates.</li>
--   </ol>
class Provable p

-- | The canonical proving function for predicate <tt>p</tt> (or a
--   canonical view function for view <tt>p</tt>).
--   
--   Note that <a>prove</a> is ambiguously typed, so you <i>always</i> need
--   to call by specifying the predicate you want to prove using
--   TypeApplications syntax:
--   
--   <pre>
--   <a>prove</a> @MyPredicate
--   </pre>
--   
--   See <a>proveTC</a> and <a>ProvableTC</a> for a version that isn't
--   ambiguously typed, but only works when <tt>p</tt> is a type
--   constructor.
prove :: Provable p => Prove p

-- | <tt><a>Disprovable</a> p</tt> is a constraint that <tt>p</tt> can be
--   disproven.
type Disprovable p = Provable (Not p)

-- | The deciding/disproving function for <tt><a>Disprovable</a> p</tt>.
--   
--   Must be called by applying the <a>Predicate</a> to disprove:
--   
--   <pre>
--   <a>disprove</a> @p
--   </pre>
disprove :: forall p. Disprovable p => Prove (Not p)

-- | If <tt>T :: k -&gt; <a>Type</a></tt> is a type constructor, then
--   <tt><a>ProvableTC</a> T</tt> is a constraint that <tt>T</tt> is
--   "decidable", in that you have a canonical function:
--   
--   <pre>
--   <a>proveTC</a> :: <a>Sing</a> a -&gt; T a
--   </pre>
--   
--   Is essentially <a>Provable</a>, except with <i>type constructors</i>
--   <tt>k -&gt; <a>Type</a></tt> instead of matchable type-level functions
--   (that are <tt>k ~&gt; <a>Type</a></tt>). Useful because <a>proveTC</a>
--   doesn't require anything fancy like TypeApplications to use.
--   
--   Also is in this library for compatiblity with "traditional" predicates
--   that are GADT type constructors.
type ProvableTC p = Provable (TyPred p)

-- | The canonical proving function for <tt><a>DecidableTC</a> t</tt>.
--   
--   Note that because <tt>t</tt> must be an injective type constructor,
--   you can use this without explicit type applications; the instance of
--   <a>ProvableTC</a> can be inferred from the result type.
proveTC :: forall t a. ProvableTC t => Sing a -> t a

-- | Implicatons <tt>p <a>--&gt;</a> q</tt> can be lifted "through" a
--   <a>TFunctor</a> into an <tt>f p <a>--&gt;</a> f q</tt>.
class TFunctor f
tmap :: forall p q. TFunctor f => (p --> q) -> f p --> f q

-- | Compose two implications.
compImpl :: forall p q r. () => (p --> q) -> (q --> r) -> p --> r

-- | A decision function for predicate <tt>p</tt>. See <a>Decidable</a> for
--   more information.
type Decide p = forall a. Sing a -> Decision (p @@ a)

-- | Like implication <a>--&gt;</a>, but knowing <tt>p @@ a</tt> can only
--   let us decidably prove <tt>q </tt><tt> a</tt> is true or false.
type p -?> q = forall a. Sing a -> p @@ a -> Decision (q @@ a)
infixr 1 -?>

-- | Like <a>-?&gt;</a>, but only in a specific context <tt>h</tt>.
type ( p -?># q ) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a))
infixr 1 -?>#

-- | A typeclass for decidable predicates.
--   
--   A predicate is decidable if, given any input <tt>a</tt>, you can
--   either prove or disprove <tt>p @@ a</tt>. A <tt><a>Decision</a> (p @@
--   a)</tt> is a data type that has a branch <tt>p @@ a</tt> and
--   <tt><a>Refuted</a> (p @@ a)</tt>.
--   
--   This typeclass associates a canonical decision function for every
--   decidable predicate.
--   
--   It confers two main advatnages:
--   
--   <ol>
--   <li>The decision function for every predicate is available via the
--   same name</li>
--   <li>We can write <a>Decidable</a> instances for polymorphic predicate
--   transformers (predicates parameterized on other predicates) easily, by
--   refering to <a>Decidable</a> instances of the transformed
--   predicates.</li>
--   </ol>
class Decidable p

-- | The canonical decision function for predicate <tt>p</tt>.
--   
--   Note that <a>decide</a> is ambiguously typed, so you <i>always</i>
--   need to call by specifying the predicate you want to prove using
--   TypeApplications syntax:
--   
--   <pre>
--   <a>decide</a> @MyPredicate
--   </pre>
--   
--   See <a>decideTC</a> and <a>DecidableTC</a> for a version that isn't
--   ambiguously typed, but only works when <tt>p</tt> is a type
--   constructor.
decide :: Decidable p => Decide p

-- | The canonical decision function for predicate <tt>p</tt>.
--   
--   Note that <a>decide</a> is ambiguously typed, so you <i>always</i>
--   need to call by specifying the predicate you want to prove using
--   TypeApplications syntax:
--   
--   <pre>
--   <a>decide</a> @MyPredicate
--   </pre>
--   
--   See <a>decideTC</a> and <a>DecidableTC</a> for a version that isn't
--   ambiguously typed, but only works when <tt>p</tt> is a type
--   constructor.
decide :: (Decidable p, Provable p) => Decide p

-- | If <tt>T :: k -&gt; <a>Type</a></tt> is a type constructor, then
--   <tt><a>DecidableTC</a> T</tt> is a constraint that <tt>T</tt> is
--   "decidable", in that you have a canonical function:
--   
--   <pre>
--   <a>decideTC</a> :: <a>Sing</a> a -&gt; <a>Decision</a> (T a)
--   </pre>
--   
--   Is essentially <a>Decidable</a>, except with <i>type constructors</i>
--   <tt>k -&gt; <a>Type</a></tt> instead of matchable type-level functions
--   (that are <tt>k ~&gt; <a>Type</a></tt>). Useful because
--   <a>decideTC</a> doesn't require anything fancy like TypeApplications
--   to use.
--   
--   Also is in this library for compatiblity with "traditional" predicates
--   that are GADT type constructors.
type DecidableTC p = Decidable (TyPred p)

-- | The canonical deciding function for <tt><a>DecidableTC</a> t</tt>.
--   
--   Note that because <tt>t</tt> must be an injective type constructor,
--   you can use this without explicit type applications; the instance of
--   <a>DecidableTC</a> can be inferred from the result type.
decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)

-- | Implicatons <tt>p <a>-?&gt;</a> q</tt> can be lifted "through" a
--   <a>DFunctor</a> into an <tt>f p <a>-?&gt;</a> f q</tt>.
class DFunctor f
dmap :: forall p q. DFunctor f => (p -?> q) -> f p -?> f q

-- | A <a>Decision</a> about a type <tt>a</tt> is either a proof of
--   existence or a proof that <tt>a</tt> cannot exist.
data () => Decision a

-- | Witness for <tt>a</tt>
Proved :: a -> Decision a

-- | Proof that no <tt>a</tt> exists
Disproved :: Refuted a -> Decision a

-- | Flip the contents of a decision. Turn a proof of <tt>a</tt> into a
--   disproof of not-<tt>a</tt>.
--   
--   Note that this is not reversible in general in constructivist logic
--   See <a>doubleNegation</a> for a situation where it is.
flipDecision :: Decision a -> Decision (Refuted a)

-- | Map over the value inside a <a>Decision</a>.
mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b

-- | Helper function for a common pattern of eliminating the disproved
--   branch of <a>Decision</a> to certaintify the proof.
elimDisproof :: Decision a -> Refuted (Refuted a) -> a

-- | Converts a <a>Decision</a> to a <a>Maybe</a>. Drop the witness of
--   disproof of <tt>a</tt>, returning <a>Just</a> if <a>Proved</a> (with
--   the proof) and <a>Nothing</a> if <a>Disproved</a>.
forgetDisproof :: Decision a -> Maybe a

-- | Drop the witness of proof of <tt>a</tt>, returning <a>Nothing</a> if
--   <a>Proved</a> and <a>Just</a> if <a>Disproved</a> (with the disproof).
forgetProof :: Decision a -> Maybe (Refuted a)

-- | Boolean test if a <a>Decision</a> is <a>Proved</a>.
isProved :: Decision a -> Bool

-- | Boolean test if a <a>Decision</a> is <a>Disproved</a>.
isDisproved :: Decision a -> Bool

-- | Change the target of a <a>Refuted</a> with a contravariant mapping
--   function.
mapRefuted :: (a -> b) -> Refuted b -> Refuted a
instance forall k (as :: [k]). (Data.Singletons.Decide.SDecide k, Data.Singletons.SingI as) => Data.Type.Predicate.Decidable (Data.Type.Predicate.In [] as)
instance forall k (as :: GHC.Maybe.Maybe k). (Data.Singletons.Decide.SDecide k, Data.Singletons.SingI as) => Data.Type.Predicate.Decidable (Data.Type.Predicate.In GHC.Maybe.Maybe as)
instance forall k j (as :: Data.Either.Either j k). (Data.Singletons.Decide.SDecide k, Data.Singletons.SingI as) => Data.Type.Predicate.Decidable (Data.Type.Predicate.In (Data.Either.Either j) as)
instance forall k (as :: GHC.Base.NonEmpty k). (Data.Singletons.Decide.SDecide k, Data.Singletons.SingI as) => Data.Type.Predicate.Decidable (Data.Type.Predicate.In GHC.Base.NonEmpty as)
instance forall k j (as :: (j, k)). (Data.Singletons.Decide.SDecide k, Data.Singletons.SingI as) => Data.Type.Predicate.Decidable (Data.Type.Predicate.In ((,) j) as)
instance forall k (as :: Data.Functor.Identity.Identity k). (Data.Singletons.Decide.SDecide k, Data.Singletons.SingI as) => Data.Type.Predicate.Decidable (Data.Type.Predicate.In Data.Functor.Identity.Identity as)
instance Data.Type.Predicate.Provable (Data.Type.Predicate.Not Data.Type.Predicate.Impossible)
instance forall k1 (p :: k1 Data.Singletons.~> *). Data.Type.Predicate.Decidable p => Data.Type.Predicate.Decidable (Data.Type.Predicate.Not p)
instance forall k (a :: k). (Data.Singletons.Decide.SDecide k, Data.Singletons.SingI a) => Data.Type.Predicate.Decidable (Data.Type.Predicate.EqualTo a)
instance Data.Type.Predicate.Decidable Data.Type.Predicate.Evident
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred Data.Singletons.WrappedSing)
instance forall u (p :: u Data.Singletons.~> *). Data.Type.Predicate.Decidable p => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Vinyl.Core.Rec (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Vinyl.Core.Rec Data.Singletons.WrappedSing))
instance forall k (p :: k Data.Singletons.~> *). Data.Type.Predicate.Decidable p => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe Data.Singletons.WrappedSing))
instance forall k (p :: k Data.Singletons.~> *). Data.Type.Predicate.Decidable p => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec Data.Singletons.WrappedSing))
instance forall k (p :: k Data.Singletons.~> *). Data.Type.Predicate.Decidable p => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity Data.Singletons.WrappedSing))
instance forall k j (p :: k Data.Singletons.~> *). Data.Type.Predicate.Decidable p => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither Data.Singletons.WrappedSing))
instance forall k j (p :: k Data.Singletons.~> *). Data.Type.Predicate.Decidable p => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup Data.Singletons.WrappedSing))
instance forall j k1 (p :: j Data.Singletons.~> *) (f :: k1 Data.Singletons.~> j). (Data.Type.Predicate.Decidable p, Data.Singletons.SingI f) => Data.Type.Predicate.Decidable (Data.Type.Predicate.PMap f p)
instance Data.Type.Predicate.Provable Data.Type.Predicate.Evident
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred Data.Singletons.WrappedSing)
instance forall u (p :: u Data.Singletons.~> *). Data.Type.Predicate.Provable p => Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Vinyl.Core.Rec (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Vinyl.Core.Rec Data.Singletons.WrappedSing))
instance forall k (p :: k Data.Singletons.~> *). Data.Type.Predicate.Provable p => Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe Data.Singletons.WrappedSing))
instance forall k (p :: k Data.Singletons.~> *). Data.Type.Predicate.Provable p => Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec Data.Singletons.WrappedSing))
instance forall k (p :: k Data.Singletons.~> *). Data.Type.Predicate.Provable p => Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity Data.Singletons.WrappedSing))
instance forall k j (p :: k Data.Singletons.~> *). Data.Type.Predicate.Provable p => Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither Data.Singletons.WrappedSing))
instance forall k j (p :: k Data.Singletons.~> *). Data.Type.Predicate.Provable p => Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup (Data.Type.Predicate.Wit p)))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup Data.Singletons.WrappedSing))
instance forall j k1 (p :: j Data.Singletons.~> *) (f :: k1 Data.Singletons.~> j). (Data.Type.Predicate.Provable p, Data.Singletons.SingI f) => Data.Type.Predicate.Provable (Data.Type.Predicate.PMap f p)


-- | Logical and algebraic connectives for predicates, as well as common
--   logical combinators.
module Data.Type.Predicate.Logic

-- | The always-true predicate.
--   
--   <pre>
--   <a>Evident</a> :: <a>Predicate</a> k
--   </pre>
data Evident :: Predicate k

-- | The always-false predicate
--   
--   Could also be defined as <tt><a>ConstSym1</a> Void</tt>, but this
--   defintion gives us a free <a>Decidable</a> instance.
--   
--   <pre>
--   <a>Impossible</a> :: <a>Predicate</a> k
--   </pre>
type Impossible = (Not Evident :: Predicate k)

-- | <tt><a>Not</a> p</tt> is the predicate that <tt>p</tt> is not true.
data Not :: Predicate k -> Predicate k

-- | Decide <tt><a>Not</a> p</tt> based on decisions of <tt>p</tt>.
decideNot :: forall p a. () => Decision (p @@ a) -> Decision (Not p @@ a)

-- | <tt>p <a>&amp;&amp;&amp;</a> q</tt> is a predicate that both
--   <tt>p</tt> and <tt>q</tt> are true.
data (&&&) :: Predicate k -> Predicate k -> Predicate k
infixr 3 &&&

-- | Decide <tt>p <a>&amp;&amp;&amp;</a> q</tt> based on decisions of
--   <tt>p</tt> and <tt>q</tt>.
decideAnd :: forall p q a. () => Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)

-- | <tt>p <a>|||</a> q</tt> is a predicate that either <tt>p</tt> and
--   <tt>q</tt> are true.
data (|||) :: Predicate k -> Predicate k -> Predicate k
infixr 2 |||

-- | Decide <tt>p <a>|||</a> q</tt> based on decisions of <tt>p</tt> and
--   <tt>q</tt>.
--   
--   Prefers <tt>p</tt> over <tt>q</tt>.
decideOr :: forall p q a. () => Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)

-- | Left-biased "or". In proofs, prioritize a proof of the left side over
--   a proof of the right side.
type p ^|| q = p ||| Not p &&& q

-- | Right-biased "or". In proofs, prioritize a proof of the right side
--   over a proof of the left side.
type p ||^ q = p &&& Not q ||| q

-- | <tt>p <a>^^^</a> q</tt> is a predicate that either <tt>p</tt> and
--   <tt>q</tt> are true, but not both.
type p ^^^ q = (p &&& Not q) ||| (Not p &&& q)

-- | Decide <tt>p <a>^^^</a> q</tt> based on decisions of <tt>p</tt> and
--   <tt>q</tt>.
decideXor :: forall p q a. () => Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)

-- | <tt>p ==&gt; q</tt> is true if <tt>q</tt> is provably true under the
--   condition that <tt>p</tt> is true.
data (==>) :: Predicate k -> Predicate k -> Predicate k
infixr 1 ==>

-- | If <tt>q</tt> is provable, then so is <tt>p <a>==&gt;</a> q</tt>.
--   
--   This can be used as an easy plug-in <a>Provable</a> instance for <tt>p
--   <a>==&gt;</a> q</tt> if <tt>q</tt> is <a>Provable</a>:
--   
--   <pre>
--   instance Provable (p ==&gt; MyPred) where
--       prove = proveImplies @MyPred
--   </pre>
--   
--   This instance isn't provided polymorphically because of overlapping
--   instance issues.
proveImplies :: Prove q -> Prove (p ==> q)

-- | <tt><a>Implies</a> p q</tt> is a constraint that <tt>p <a>==&gt;</a>
--   q</tt> is <a>Provable</a>; that is, you can prove that <tt>p</tt>
--   implies <tt>q</tt>.
type Implies p q = Provable (p ==> q)

-- | Two-way implication, or logical equivalence
type p <==> q = p ==> q &&& q ==> p
infixr 1 <==>

-- | <tt><a>Equiv</a> p q</tt> is a constraint that <tt>p <a>&lt;==&gt;</a>
--   q</tt> is <a>Provable</a>; that is, you can prove that <tt>p</tt> is
--   logically equivalent to <tt>q</tt>.
type Equiv p q = Provable (p <==> q)

-- | Compose two implications.
compImpl :: forall p q r. () => (p --> q) -> (q --> r) -> p --> r

-- | From <tt><a>Impossible</a> </tt><tt> a</tt>, you can prove anything.
--   Essentially a lifted version of <a>absurd</a>.
explosion :: Impossible --> p

-- | <a>Evident</a> can be proven from all predicates.
atom :: p --> Evident

-- | We cannot have both <tt>p</tt> and <tt><a>Not</a> p</tt>.
--   
--   (Renamed in v0.1.4.0; used to be <tt>excludedMiddle</tt>)
complementation :: forall p. (p &&& Not p) --> Impossible

-- | Logical double negation. Only possible if <tt>p</tt> is
--   <a>Decidable</a>.
--   
--   This is because in constructivist logic, not (not p) does not imply p.
--   However, p implies not (not p) (see <a>negateTwice</a>), and not (not
--   (not p)) implies not p (see <a>tripleNegation</a>)
doubleNegation :: forall p. Decidable p => Not (Not p) --> p

-- | In constructivist logic, not (not (not p)) implies not p.
tripleNegation :: forall p. Not (Not (Not p)) --> Not p

-- | In constructivist logic, p implies not (not p).
negateTwice :: p --> Not (Not p)

-- | If p implies q, then not q implies not p.
contrapositive :: (p --> q) -> Not q --> Not p

-- | Reverse direction of <a>contrapositive</a>. Only possible if
--   <tt>q</tt> is <a>Decidable</a> on its own, without the help of
--   <tt>p</tt>, which makes this much less useful.
contrapositive' :: forall p q. Decidable q => (Not q --> Not p) -> p --> q

-- | If <tt>p <a>&amp;&amp;&amp;</a> q</tt> is true, then so is <tt>p</tt>.
projAndFst :: (p &&& q) --> p

-- | If <tt>p <a>&amp;&amp;&amp;</a> q</tt> is true, then so is <tt>q</tt>.
projAndSnd :: (p &&& q) --> q

-- | If <tt>p</tt> is true, then so is <tt>p <a>|||</a> q</tt>.
injOrLeft :: forall p q. p --> (p ||| q)

-- | If <tt>q</tt> is true, then so is <tt>p <a>|||</a> q</tt>.
injOrRight :: forall p q. q --> (p ||| q)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable (Data.Type.Predicate.Impossible Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (Data.Type.Predicate.Impossible Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). (Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.==> q), Data.Type.Predicate.Decidable q) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Not q Data.Type.Predicate.Logic.==> Data.Type.Predicate.Not p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (p Data.Type.Predicate.Logic.==> q) => Data.Type.Predicate.Provable (Data.Type.Predicate.Not q Data.Type.Predicate.Logic.==> Data.Type.Predicate.Not p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable ((p Data.Type.Predicate.Logic.&&& q) Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable ((p Data.Type.Predicate.Logic.&&& q) Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable ((p Data.Type.Predicate.Logic.&&& q) Data.Type.Predicate.Logic.==> q)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable ((p Data.Type.Predicate.Logic.&&& q) Data.Type.Predicate.Logic.==> q)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable ((p Data.Type.Predicate.Logic.&&& p) Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable ((p Data.Type.Predicate.Logic.&&& p) Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| q))
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (p Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| q))
instance forall k1 (q :: Data.Type.Predicate.Predicate k1) (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable (q Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| q))
instance forall k1 (q :: Data.Type.Predicate.Predicate k1) (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (q Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| q))
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| p))
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (p Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| p))
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable ((p Data.Type.Predicate.Logic.&&& Data.Type.Predicate.Not p) Data.Type.Predicate.Logic.==> Data.Type.Predicate.Impossible)
instance forall k1 (p :: k1 Data.Singletons.~> *) (q :: k1 Data.Singletons.~> *). (Data.Type.Predicate.Decidable p, Data.Type.Predicate.Decidable q) => Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.||| q)
instance forall k1 (p :: k1 Data.Singletons.~> *) (q :: k1 Data.Singletons.~> *). (Data.Type.Predicate.Decidable p, Data.Type.Predicate.Decidable q) => Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.&&& q)
instance forall k1 (p :: k1 Data.Singletons.~> *) (q :: k1 Data.Singletons.~> *). (Data.Type.Predicate.Provable p, Data.Type.Predicate.Provable q) => Data.Type.Predicate.Provable (p Data.Type.Predicate.Logic.&&& q)


-- | A type family for "containers", intended for allowing lifting of
--   predicates on <tt>k</tt> to be predicates on containers <tt>f k</tt>.
module Data.Type.Universe
type family Elem (f :: Type -> Type) = (i :: f k -> k -> Type) | i -> f

-- | <tt><a>In</a> f as</tt> is a predicate that a given input <tt>a</tt>
--   is a member of collection <tt>as</tt>.
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as

-- | Typeclass for a type-level container that you can quantify or lift
--   type-level predicates over.
class FProd f => Universe (f :: Type -> Type)

-- | <a>decideAny</a>, but providing an <a>Elem</a>.
idecideAny :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any f p @@ as)

-- | <a>decideAll</a>, but providing an <a>Elem</a>.
idecideAll :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All f p @@ as)
allProd :: forall p g. Universe f => (forall a. Sing a -> (p @@ a) -> g a) -> All f p --> TyPred (Prod f g)
prodAll :: forall p g as. Universe f => (forall a. g a -> p @@ a) -> Prod f g as -> All f p @@ as

-- | Split a <tt><a>Sing</a> as</tt> into a proof that all <tt>a</tt> in
--   <tt>as</tt> exist.
singAll :: forall f k (as :: f k). Universe f => Sing as -> All f Evident @@ as

-- | Witness an item in a type-level list by providing its index.
--   
--   The number of <a>IS</a>s correspond to the item's position in the
--   list.
--   
--   <pre>
--   <a>IZ</a>         :: <a>Index</a> '[5,10,2] 5
--   <a>IS</a> <a>IZ</a>      :: <a>Index</a> '[5,10,2] 10
--   <a>IS</a> (<a>IS</a> <a>IZ</a>) :: <a>Index</a> '[5,10,2] 2
--   </pre>
data () => Index (a :: [k]) (b :: k)
[IZ] :: forall {k} (b :: k) (as :: [k]). Index (b ': as) b
[IS] :: forall {k} (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 ': bs) b

-- | Witness an item in a type-level <a>Maybe</a> by proving the
--   <a>Maybe</a> is <a>Just</a>.
data () => IJust (a :: Maybe k) (b :: k)
[IJust] :: forall {k} (b :: k). IJust ('Just b) b

-- | Witness an item in a type-level <tt><a>Either</a> j</tt> by proving
--   the <a>Either</a> is <a>Right</a>.
data () => IRight (a :: Either j k) (b :: k)
[IRight] :: forall {k} {j} (b :: k). IRight ('Right b :: Either j k) b

-- | Witness an item in a type-level <a>NonEmpty</a> by either indicating
--   that it is the "head", or by providing an index in the "tail".
data () => NEIndex (a :: NonEmpty k) (b :: k)
[NEHead] :: forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
[NETail] :: forall {k} (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 ':| as) b

-- | Trivially witness an item in the second field of a type-level tuple.
data () => ISnd (a :: (j, k)) (b :: k)
[ISnd] :: forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b

-- | Trivially witness the item held in an <a>Identity</a>.
data () => IIdentity (a :: Identity k) (b :: k)
[IId] :: forall {k} (b :: k). IIdentity ('Identity b) b

-- | An <tt><a>All</a> f p</tt> is a predicate testing a collection <tt>as
--   :: f a</tt> for the fact that <i>all</i> items in <tt>as</tt> satisfy
--   <tt>p</tt>. Represents the "forall" quantifier over a given universe.
--   
--   This is mostly useful for its <a>Decidable</a>, <a>Provable</a>, and
--   <a>TFunctor</a> instances, which lets you lift predicates on
--   <tt>p</tt> to predicates on <tt><a>All</a> f p</tt>.
data All f :: Predicate k -> Predicate (f k)

-- | A <tt><a>WitAll</a> p as</tt> is a witness that the predicate <tt>p
--   a</tt> is true for all items <tt>a</tt> in the type-level collection
--   <tt>as</tt>.
newtype WitAll f p (as :: f k)
WitAll :: (forall a. Elem f as a -> p @@ a) -> WitAll f p (as :: f k)
[runWitAll] :: WitAll f p (as :: f k) -> forall a. Elem f as a -> p @@ a

-- | A <tt><a>NotAll</a> f p</tt> is a predicate on a collection
--   <tt>as</tt> that at least one <tt>a</tt> in <tt>as</tt> does not
--   satisfy predicate <tt>p</tt>.
type NotAll f p = (Not (All f p) :: Predicate (f k))

-- | An <tt><a>Any</a> f p</tt> is a predicate testing a collection <tt>as
--   :: f a</tt> for the fact that at least one item in <tt>as</tt>
--   satisfies <tt>p</tt>. Represents the "exists" quantifier over a given
--   universe.
--   
--   This is mostly useful for its <a>Decidable</a> and <a>TFunctor</a>
--   instances, which lets you lift predicates on <tt>p</tt> to predicates
--   on <tt><a>Any</a> f p</tt>.
data Any f :: Predicate k -> Predicate (f k)

-- | A <tt><a>WitAny</a> p as</tt> is a witness that, for at least one item
--   <tt>a</tt> in the type-level collection <tt>as</tt>, the predicate
--   <tt>p a</tt> is true.
data WitAny f :: (k ~> Type) -> f k -> Type
[WitAny] :: Elem f as a -> (p @@ a) -> WitAny f p as

-- | A <tt><a>None</a> f p</tt> is a predicate on a collection <tt>as</tt>
--   that no <tt>a</tt> in <tt>as</tt> satisfies predicate <tt>p</tt>.
type None f p = (Not (Any f p) :: Predicate (f k))

-- | Predicate that a given <tt>as :: f k</tt> is empty and has no items in
--   it.
type Null f = (None f Evident :: Predicate (f k))

-- | Predicate that a given <tt>as :: f k</tt> is not empty, and has at
--   least one item in it.
type NotNull f = (Any f Evident :: Predicate (f k))

-- | Test that a <a>Maybe</a> is <a>Just</a>.
type IsJust = (NotNull Maybe :: Predicate (Maybe k))

-- | Test that a <a>Maybe</a> is <a>Nothing</a>.
type IsNothing = (Null Maybe :: Predicate (Maybe k))

-- | Test that an <a>Either</a> is <a>Right</a>
type IsRight = (NotNull (Either j) :: Predicate (Either j k))

-- | Test that an <a>Either</a> is <a>Left</a>
type IsLeft = (Null (Either j) :: Predicate (Either j k))

-- | Lifts a predicate <tt>p</tt> on an individual <tt>a</tt> into a
--   predicate that on a collection <tt>as</tt> that is true if and only if
--   <i>any</i> item in <tt>as</tt> satisfies the original predicate.
--   
--   That is, it turns a predicate of kind <tt>k ~&gt; Type</tt> into a
--   predicate of kind <tt>f k ~&gt; Type</tt>.
--   
--   Essentially tests existential quantification.
decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)

-- | Lifts a predicate <tt>p</tt> on an individual <tt>a</tt> into a
--   predicate that on a collection <tt>as</tt> that is true if and only if
--   <i>all</i> items in <tt>as</tt> satisfies the original predicate.
--   
--   That is, it turns a predicate of kind <tt>k ~&gt; Type</tt> into a
--   predicate of kind <tt>f k ~&gt; Type</tt>.
--   
--   Essentially tests universal quantification.
decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)

-- | If <tt>p a</tt> is true for all values <tt>a</tt> in <tt>as</tt>, then
--   we have <tt><a>All</a> p as</tt>. Basically witnesses the definition
--   of <a>All</a>.
genAll :: forall f k (p :: k ~> Type). Universe f => Prove p -> Prove (All f p)

-- | <a>genAll</a>, but providing an <a>Elem</a>.
igenAll :: forall f k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> p @@ a) -> Sing as -> All f p @@ as

-- | Split a <tt><a>Sing</a> as</tt> into a proof that all <tt>a</tt> in
--   <tt>as</tt> exist.
splitSing :: forall f k (as :: f k). Universe f => Sing as -> All f (TyPred Sing) @@ as

-- | Automatically generate a witness for a member, if possible
pickElem :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k) => Decision (Elem f as a)
instance forall k (f :: * -> *) (p :: k Data.Singletons.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Decidable (Data.Type.Universe.NotNull f Data.Type.Predicate.Logic.==> Data.Type.Universe.Any f p)
instance forall k (p :: k Data.Singletons.~> *) (f :: * -> *). Data.Type.Predicate.Provable p => Data.Type.Predicate.Provable (Data.Type.Universe.NotNull f Data.Type.Predicate.Logic.==> Data.Type.Universe.Any f p)
instance forall k (f :: * -> *) (p :: k Data.Singletons.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Decidable (Data.Type.Universe.Any f p)
instance forall k (f :: * -> *) (p :: k Data.Singletons.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Decidable (Data.Type.Universe.All f p)
instance forall k (f :: * -> *) (p :: k Data.Singletons.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Provable (Data.Type.Universe.All f p)
instance Data.Type.Universe.Universe f => Data.Type.Predicate.TFunctor (Data.Type.Universe.Any f)
instance Data.Type.Universe.Universe f => Data.Type.Predicate.TFunctor (Data.Type.Universe.All f)
instance Data.Type.Universe.Universe f => Data.Type.Predicate.DFunctor (Data.Type.Universe.All f)
instance Data.Type.Universe.Universe []
instance Data.Type.Universe.Universe GHC.Maybe.Maybe
instance Data.Type.Universe.Universe (Data.Either.Either j)
instance Data.Type.Universe.Universe GHC.Base.NonEmpty
instance Data.Type.Universe.Universe ((,) j)
instance Data.Type.Universe.Universe Data.Functor.Identity.Identity


-- | Higher-level predicates for quantifying predicates over universes and
--   sets.
module Data.Type.Predicate.Quantification

-- | An <tt><a>Any</a> f p</tt> is a predicate testing a collection <tt>as
--   :: f a</tt> for the fact that at least one item in <tt>as</tt>
--   satisfies <tt>p</tt>. Represents the "exists" quantifier over a given
--   universe.
--   
--   This is mostly useful for its <a>Decidable</a> and <a>TFunctor</a>
--   instances, which lets you lift predicates on <tt>p</tt> to predicates
--   on <tt><a>Any</a> f p</tt>.
data Any f :: Predicate k -> Predicate (f k)

-- | A <tt><a>WitAny</a> p as</tt> is a witness that, for at least one item
--   <tt>a</tt> in the type-level collection <tt>as</tt>, the predicate
--   <tt>p a</tt> is true.
data WitAny f :: (k ~> Type) -> f k -> Type
[WitAny] :: Elem f as a -> (p @@ a) -> WitAny f p as

-- | A <tt><a>None</a> f p</tt> is a predicate on a collection <tt>as</tt>
--   that no <tt>a</tt> in <tt>as</tt> satisfies predicate <tt>p</tt>.
type None f p = (Not (Any f p) :: Predicate (f k))

-- | It is impossible for any value in a collection to be
--   <a>Impossible</a>.
anyImpossible :: Universe f => Any f Impossible --> Impossible

-- | Lifts a predicate <tt>p</tt> on an individual <tt>a</tt> into a
--   predicate that on a collection <tt>as</tt> that is true if and only if
--   <i>any</i> item in <tt>as</tt> satisfies the original predicate.
--   
--   That is, it turns a predicate of kind <tt>k ~&gt; Type</tt> into a
--   predicate of kind <tt>f k ~&gt; Type</tt>.
--   
--   Essentially tests existential quantification.
decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)

-- | <a>decideAny</a>, but providing an <a>Elem</a>.
idecideAny :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any f p @@ as)

-- | Lifts a predicate <tt>p</tt> on an individual <tt>a</tt> into a
--   predicate that on a collection <tt>as</tt> that is true if and only if
--   <i>no</i> item in <tt>as</tt> satisfies the original predicate.
--   
--   That is, it turns a predicate of kind <tt>k ~&gt; Type</tt> into a
--   predicate of kind <tt>f k ~&gt; Type</tt>.
decideNone :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (None f p)

-- | <a>decideNone</a>, but providing an <a>Elem</a>.
idecideNone :: forall f k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (None f p @@ as)

-- | If there exists an <tt>a</tt> s.t. <tt>p a</tt>, and if <tt>p</tt>
--   implies <tt>q</tt>, then there must exist an <tt>a</tt> s.t. <tt>q
--   a</tt>.
entailAny :: forall f p q. Universe f => (p --> q) -> Any f p --> Any f q

-- | <a>entailAny</a>, but providing an <a>Elem</a>.
ientailAny :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> Sing a -> (p @@ a) -> q @@ a) -> (Any f p @@ as) -> Any f q @@ as

-- | If <tt>p</tt> implies <tt>q</tt> under some context <tt>h</tt>, and if
--   there exists some <tt>a</tt> such that <tt>p a</tt>, then there must
--   exist some <tt>a</tt> such that <tt>p q</tt> under that context
--   <tt>h</tt>.
--   
--   <tt>h</tt> might be something like, say, <a>Maybe</a>, to give
--   predicate that is either provably true or unprovably false.
--   
--   Note that it is not possible to do this with <tt>p a -&gt;
--   <a>Decision</a> (q a)</tt>. This is if the <tt>p a -&gt;
--   <a>Decision</a> (q a)</tt> implication is false, there it doesn't mean
--   that there is <i>no</i> <tt>a</tt> such that <tt>q a</tt>,
--   necessarily. There could have been an <tt>a</tt> where <tt>p</tt> does
--   not hold, but <tt>q</tt> does.
entailAnyF :: forall f p q h. (Universe f, Functor h) => (p --># q) h -> (Any f p --># Any f q) h

-- | <a>entailAnyF</a>, but providing an <a>Elem</a>.
ientailAnyF :: forall f p q as h. Functor h => (forall a. Elem f as a -> (p @@ a) -> h (q @@ a)) -> (Any f p @@ as) -> h (Any f q @@ as)

-- | An <tt><a>All</a> f p</tt> is a predicate testing a collection <tt>as
--   :: f a</tt> for the fact that <i>all</i> items in <tt>as</tt> satisfy
--   <tt>p</tt>. Represents the "forall" quantifier over a given universe.
--   
--   This is mostly useful for its <a>Decidable</a>, <a>Provable</a>, and
--   <a>TFunctor</a> instances, which lets you lift predicates on
--   <tt>p</tt> to predicates on <tt><a>All</a> f p</tt>.
data All f :: Predicate k -> Predicate (f k)

-- | A <tt><a>WitAll</a> p as</tt> is a witness that the predicate <tt>p
--   a</tt> is true for all items <tt>a</tt> in the type-level collection
--   <tt>as</tt>.
newtype WitAll f p (as :: f k)
WitAll :: (forall a. Elem f as a -> p @@ a) -> WitAll f p (as :: f k)
[runWitAll] :: WitAll f p (as :: f k) -> forall a. Elem f as a -> p @@ a

-- | A <tt><a>NotAll</a> f p</tt> is a predicate on a collection
--   <tt>as</tt> that at least one <tt>a</tt> in <tt>as</tt> does not
--   satisfy predicate <tt>p</tt>.
type NotAll f p = (Not (All f p) :: Predicate (f k))

-- | Lifts a predicate <tt>p</tt> on an individual <tt>a</tt> into a
--   predicate that on a collection <tt>as</tt> that is true if and only if
--   <i>all</i> items in <tt>as</tt> satisfies the original predicate.
--   
--   That is, it turns a predicate of kind <tt>k ~&gt; Type</tt> into a
--   predicate of kind <tt>f k ~&gt; Type</tt>.
--   
--   Essentially tests universal quantification.
decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)

-- | <a>decideAll</a>, but providing an <a>Elem</a>.
idecideAll :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All f p @@ as)

-- | If for all <tt>a</tt> we have <tt>p a</tt>, and if <tt>p</tt> implies
--   <tt>q</tt>, then for all <tt>a</tt> we must also have <tt>p a</tt>.
entailAll :: forall f p q. Universe f => (p --> q) -> All f p --> All f q

-- | <a>entailAll</a>, but providing an <a>Elem</a>.
ientailAll :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> Sing a -> (p @@ a) -> q @@ a) -> (All f p @@ as) -> All f q @@ as

-- | If <tt>p</tt> implies <tt>q</tt> under some context <tt>h</tt>, and if
--   we have <tt>p a</tt> for all <tt>a</tt>, then we must have <tt>q
--   a</tt> for all <tt>a</tt> under context <tt>h</tt>.
entailAllF :: forall f p q h. (Universe f, Applicative h) => (p --># q) h -> (All f p --># All f q) h

-- | <a>entailAllF</a>, but providing an <a>Elem</a>.
ientailAllF :: forall f p q as h. (Universe f, Applicative h, SingI as) => (forall a. Elem f as a -> (p @@ a) -> h (q @@ a)) -> (All f p @@ as) -> h (All f q @@ as)

-- | If we have <tt>p a</tt> for all <tt>a</tt>, and <tt>p a</tt> can be
--   used to test for <tt>q a</tt>, then we can test all <tt>a</tt>s for
--   <tt>q a</tt>.
decideEntailAll :: forall f p q. Universe f => (p -?> q) -> All f p -?> All f q

-- | <a>entailAllF</a>, but providing an <a>Elem</a>.
idecideEntailAll :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> (p @@ a) -> Decision (q @@ a)) -> (All f p @@ as) -> Decision (All f q @@ as)

-- | If something is true for all xs, then it must be true for at least one
--   x in xs, provided that xs is not empty.
allToAny :: (All f p &&& NotNull f) --> Any f p

-- | If <tt>p</tt> is false for all <tt>a</tt> in <tt>as</tt>, then no
--   <tt>a</tt> in <tt>as</tt> satisfies <tt>p</tt>.
allNotNone :: All f (Not p) --> None f p

-- | If no <tt>a</tt> in <tt>as</tt> satisfies <tt>p</tt>, then <tt>p</tt>
--   is false for all <tt>a</tt> in <tt>as</tt>. Requires
--   <tt><a>Decidable</a> p</tt> to interrogate the input disproof.
noneAllNot :: forall f p. (Universe f, Decidable p) => None f p --> All f (Not p)

-- | If any <tt>a</tt> in <tt>as</tt> does not satisfy <tt>p</tt>, then not
--   all <tt>a</tt> in <tt>as</tt> satisfy <tt>p</tt>.
anyNotNotAll :: Any f (Not p) --> NotAll f p

-- | If not all <tt>a</tt> in <tt>as</tt> satisfy <tt>p</tt>, then there
--   must be at least one <tt>a</tt> in <tt>as</tt> that does not satisfy
--   <tt>p</tt>. Requires <tt><a>Decidable</a> p</tt> in order to locate
--   that specific <tt>a</tt>.
notAllAnyNot :: forall f p. (Universe f, Decidable p) => NotAll f p --> Any f (Not p)


-- | Manipulate "parameterized predicates". See <a>ParamPred</a> and
--   <a>Found</a> for more information.
module Data.Type.Predicate.Param

-- | A parameterized predicate. See <a>Found</a> for more information.
type ParamPred k v = k -> Predicate v

-- | <tt>Found (<a>IsTC</a> t) @@ x</tt> is true if <tt>x</tt> was made
--   using the unary type constructor <tt>t</tt>.
--   
--   For example:
--   
--   <pre>
--   type IsJust = (Found (IsTC 'Just) :: Predicate (Maybe v))
--   </pre>
--   
--   makes a predicate where <tt>IsJust @@ x</tt> is true if <tt>x</tt> is
--   <a>Just</a>, and false if <tt>x</tt> is <a>Nothing</a>.
--   
--   For a more general version, see <a>EqBy</a>
--   
--   The kind of <a>IsTC</a> is:
--   
--   <pre>
--   <a>IsTC</a> :: (v -&gt; k) -&gt; <a>ParamPred</a> k v
--   <a>Found</a> (<a>IsTC</a> t) :: <a>Predicate</a> k
--   </pre>
--   
--   Applied to specific things:
--   
--   <pre>
--   <a>IsTC</a> '<a>Just</a> :: <a>ParamPred</a> (Maybe v) v
--   <a>Found</a> (<a>IsTC</a> '<tt>Just'</tt>) :: <a>Predicate</a> (Maybe v)
--   </pre>
type IsTC t = EqBy (TyCon1 t)

-- | <tt>Found (<a>EqBy</a> f) @@ x</tt> is true if there exists some value
--   when, with <tt>f</tt> applied to it, is equal to <tt>x</tt>.
--   
--   See <a>IsTC</a> for a useful specific application.
--   
--   <pre>
--   <a>EqBy</a> :: (v ~&gt; k) -&gt; <a>ParamPred</a> k v
--   <a>Found</a> (<a>EqBy</a> f) :: <a>Predicate</a> k
--   </pre>
data EqBy :: (v ~> k) -> ParamPred k v

-- | Flip the arguments of a <a>ParamPred</a>.
data FlipPP :: ParamPred v k -> ParamPred k v

-- | Promote a <tt><a>Predicate</a> v</tt> to a <tt><a>ParamPred</a> k
--   v</tt>, ignoring the <tt>k</tt> input.
data ConstPP :: Predicate v -> ParamPred k v

-- | Pre-compose a function to a <a>ParamPred</a>. Is essentially
--   <tt><a>flip</a> (<a>.</a>)</tt>, but unfortunately defunctionalization
--   doesn't work too well with that definition.
data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v

-- | Pre-compose a function to a <a>ParamPred</a>, but on the "value" side.
data PPMapV :: (u ~> v) -> ParamPred k u -> ParamPred k v

-- | A <tt><a>ParamPred</a> (f k) k</tt>. Parameterized on an <tt>as :: f
--   k</tt>, returns a predicate that is true if there exists any <tt>a ::
--   k</tt> in <tt>as</tt>.
--   
--   Essentially <a>NotNull</a>.
type InP f = (ElemSym1 f :: ParamPred (f k) k)

-- | <tt><a>AnyMatch</a> f</tt> takes a parmaeterized predicate on
--   <tt>k</tt> (testing for a <tt>v</tt>) and turns it into a
--   parameterized predicate on <tt>f k</tt> (testing for a <tt>v</tt>). It
--   "lifts" the domain into <tt>f</tt>.
--   
--   An <tt><a>AnyMatch</a> f p as</tt> is a predicate taking an argument
--   <tt>a</tt> and testing if <tt>p a :: <a>Predicate</a> k</tt> is
--   satisfied for any item in <tt>as :: f k</tt>.
--   
--   A <tt><a>ParamPred</a> k v</tt> tests if a <tt>k</tt> can create some
--   <tt>v</tt>. The resulting <tt><a>ParamPred</a> (f k) v</tt> tests if
--   any <tt>k</tt> in <tt>f k</tt> can create some <tt>v</tt>.
data AnyMatch f :: ParamPred k v -> ParamPred (f k) v

-- | Convert a normal <tt>-&gt;</tt> type constructor taking two arguments
--   into a <a>ParamPred</a>.
--   
--   <pre>
--   <a>TyPP</a> :: (k -&gt; v -&gt; <a>Type</a>) -&gt; <a>ParamPred</a> k v
--   </pre>
data TyPP :: (k -> v -> Type) -> ParamPred k v

-- | Convert a parameterized predicate into a predicate on the parameter.
--   
--   A <tt><a>Found</a> p</tt> is a predicate on <tt>p :: <a>ParamPred</a>
--   k v</tt> that tests a <tt>k</tt> for the fact that there exists a
--   <tt>v</tt> where <tt><a>ParamPred</a> k v</tt> is satisfied.
--   
--   Intended as the basic interface for <a>ParamPred</a>, since it turns a
--   <a>ParamPred</a> into a normal <a>Predicate</a>, which can have
--   <a>Decidable</a> and <a>Provable</a> instances.
--   
--   For some context, an instance of <tt><a>Provable</a> (<a>Found</a>
--   P)</tt>, where <tt>P :: <a>ParamPred</a> k v</tt>, means that for any
--   input <tt>x :: k</tt>, we can always find a <tt>y :: v</tt> such that
--   we have <tt>P x @@ y</tt>.
--   
--   In the language of quantifiers, it means that forall <tt>x :: k</tt>,
--   there exists a <tt>y :: v</tt> such that <tt>P x @@ y</tt>.
--   
--   For an instance of <tt><a>Decidable</a> (<a>Found</a> P)</tt>, it
--   means that for all <tt>x :: k</tt>, we can prove or disprove the fact
--   that there exists a <tt>y :: v</tt> such that <tt>P x @@ y</tt>.
data Found :: ParamPred k v -> Predicate k

-- | Convert a parameterized predicate into a predicate on the parameter.
--   
--   A <tt><a>Found</a> p</tt> is a predicate on <tt>p :: <a>ParamPred</a>
--   k v</tt> that tests a <tt>k</tt> for the fact that there <i>cannot
--   exist</i> a <tt>v</tt> where <tt><a>ParamPred</a> k v</tt> is
--   satisfied. That is, <tt><a>NotFound</a> P @@ x</tt> is satisfied if no
--   <tt>y :: v</tt> can exist where <tt>P x @@ y</tt> is satisfied.
--   
--   For some context, an instance of <tt><a>Provable</a> (<a>NotFound</a>
--   P)</tt>, where <tt>P :: <a>ParamPred</a> k v</tt>, means that for any
--   input <tt>x :: k</tt>, we can always reject any <tt>y :: v</tt> that
--   claims to satisfy <tt>P x @@ y</tt>.
--   
--   In the language of quantifiers, it means that forall <tt>x :: k</tt>,
--   there does not exist a <tt>y :: v</tt> such that <tt>P x @@ y</tt>.
--   
--   For an instance of <tt><a>Decidable</a> (<a>Found</a> P)</tt>, it
--   means that for all <tt>x :: k</tt>, we can prove or disprove the fact
--   that there does not exist a <tt>y :: v</tt> such that <tt>P x @@
--   y</tt>.
type NotFound (p :: ParamPred k v) = (Not (Found p) :: Predicate k)

-- | A constraint that a <tt><a>ParamPred</a> k v</tt> s "selectable". It
--   means that for any input <tt>x :: k</tt>, we can always find a <tt>y
--   :: v</tt> that satisfies <tt>P x @@ y</tt>. We can "select" that
--   <tt>y</tt>, no matter what.
type Selectable p = Provable (Found p)

-- | The proving/selecting function for <tt><a>Selectable</a> p</tt>.
--   
--   Because this is ambiguously typed, it must be called by applying the
--   <a>ParamPred</a>:
--   
--   <pre>
--   <a>select</a> @p
--   </pre>
--   
--   See <a>selectTC</a> and <a>SelectableTC</a> for a version that isn't
--   ambiguously typed, but only works when <tt>p</tt> is a type
--   constructor.
select :: forall p. Selectable p => Prove (Found p)

-- | A constraint that a <tt><a>ParamPred</a> k v</tt> is "searchable". It
--   means that for any input <tt>x :: k</tt>, we can prove or disprove
--   that there exists a <tt>y :: v</tt> that satisfies <tt>P x @@ y</tt>.
--   We can "search" for that <tt>y</tt>, and prove that it can or cannot
--   be found.
type Searchable p = Decidable (Found p)

-- | The deciding/searching function for <tt><a>Searchable</a> p</tt>.
--   
--   Because this is ambiguously typed, it must be called by applying the
--   <a>ParamPred</a>:
--   
--   <pre>
--   <a>search</a> @p
--   </pre>
--   
--   See <a>searchTC</a> and <a>SearchableTC</a> for a version that isn't
--   ambiguously typed, but only works when <tt>p</tt> is a type
--   constructor.
search :: forall p. Searchable p => Decide (Found p)

-- | <tt><a>NotNull</a> f</tt> is basically <tt><a>Found</a> (<a>InP</a>
--   f)</tt>.
inPNotNull :: Found (InP f) --> NotNull f

-- | <tt><a>NotNull</a> f</tt> is basically <tt><a>Found</a> (<a>InP</a>
--   f)</tt>.
notNullInP :: NotNull f --> Found (InP f)

-- | If <tt>T :: k -&gt; v -&gt; <a>Type</a></tt> is a type constructor,
--   then <tt><a>Selectable</a> T</tt> is a constraint that <tt>T</tt> is
--   "selectable", in that you have a canonical function:
--   
--   <pre>
--   <a>selectTC</a> :: <a>Sing</a> a -&gt; Σ v (<a>TyPP</a> T x)
--   </pre>
--   
--   That is, given an <tt>x :: k</tt>, we can <i>always</i> find a <tt>y
--   :: k</tt> that satisfies <tt>T x y</tt>.
--   
--   Is essentially <a>Selectable</a>, except with <i>type constructors</i>
--   <tt>k -&gt; <a>Type</a></tt> instead of matchable type-level functions
--   (that are <tt>k ~&gt; <a>Type</a></tt>). Useful because
--   <a>selectTC</a> doesn't require anything fancy like TypeApplications
--   to use.
type SelectableTC t = Provable (Found (TyPP t))

-- | The canonical selecting function for <tt><a>SelectableTC</a> t</tt>.
--   
--   Note that because <tt>t</tt> must be an injective type constructor,
--   you can use this without explicit type applications; the instance of
--   <a>SelectableTC</a> can be inferred from the result type.
selectTC :: forall t. SelectableTC t => Prove (Found (TyPP t))

-- | If <tt>T :: k -&gt; v -&gt; <a>Type</a></tt> is a type constructor,
--   then <tt><a>SearchableTC</a> T</tt> is a constraint that <tt>T</tt> is
--   "searchable", in that you have a canonical function:
--   
--   <pre>
--   <a>searchTC</a> :: <a>Sing</a> x -&gt; <a>Decision</a> (Σ v (<a>TyPP</a> T x))
--   </pre>
--   
--   That, given an <tt>x :: k</tt>, we can decide whether or not a <tt>y
--   :: v</tt> exists that satisfies <tt>T x y</tt>.
--   
--   Is essentially <a>Searchable</a>, except with <i>type constructors</i>
--   <tt>k -&gt; <a>Type</a></tt> instead of matchable type-level functions
--   (that are <tt>k ~&gt; <a>Type</a></tt>). Useful because
--   <a>searchTC</a> doesn't require anything fancy like TypeApplications
--   to use.
type SearchableTC t = Decidable (Found (TyPP t))

-- | The canonical selecting function for <tt><a>Searchable</a> t</tt>.
--   
--   Note that because <tt>t</tt> must be an injective type constructor,
--   you can use this without explicit type applications; the instance of
--   <a>SearchableTC</a> can be inferred from the result type.
searchTC :: forall t. SearchableTC t => Decide (Found (TyPP t))

-- | Disjunction on two <a>ParamPred</a>s, with appropriate
--   <a>Searchable</a> instance. Priority is given to the left predicate.
data OrP :: ParamPred k v -> ParamPred k v -> ParamPred k v

-- | Conjunction on two <a>ParamPred</a>s, with appropriate
--   <a>Searchable</a> and <a>Selectable</a> instances.
data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u)
instance forall k1 v u (p :: Data.Type.Predicate.Param.ParamPred k1 v) (q :: Data.Type.Predicate.Param.ParamPred k1 u). (Data.Type.Predicate.Param.Searchable p, Data.Type.Predicate.Param.Searchable q) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.AndP p q))
instance forall k1 v u (p :: Data.Type.Predicate.Param.ParamPred k1 v) (q :: Data.Type.Predicate.Param.ParamPred k1 u). (Data.Type.Predicate.Param.Selectable p, Data.Type.Predicate.Param.Selectable q) => Data.Type.Predicate.Provable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.AndP p q))
instance forall k1 v (p :: Data.Type.Predicate.Param.ParamPred k1 v) (q :: Data.Type.Predicate.Param.ParamPred k1 v). (Data.Type.Predicate.Param.Searchable p, Data.Type.Predicate.Param.Searchable q) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.OrP p q))
instance forall k v (f :: * -> *) (p :: Data.Type.Predicate.Param.ParamPred k v). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found p)) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.AnyMatch f p))
instance Data.Type.Universe.Universe f => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f))
instance Data.Type.Predicate.Decidable (Data.Type.Universe.NotNull f Data.Type.Predicate.Logic.==> Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f))
instance Data.Type.Predicate.Provable (Data.Type.Universe.NotNull f Data.Type.Predicate.Logic.==> Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f) Data.Type.Predicate.Logic.==> Data.Type.Universe.NotNull f)
instance Data.Type.Predicate.Provable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f) Data.Type.Predicate.Logic.==> Data.Type.Universe.NotNull f)
instance forall j v (p :: Data.Type.Predicate.Param.ParamPred j v) k (f :: k Data.Singletons.~> j). (Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found p), Data.Singletons.SingI f) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.PPMap f p))
instance forall j v (p :: Data.Type.Predicate.Param.ParamPred j v) k (f :: k Data.Singletons.~> j). (Data.Type.Predicate.Provable (Data.Type.Predicate.Param.Found p), Data.Singletons.SingI f) => Data.Type.Predicate.Provable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.PPMap f p))


-- | Useful utilities for situations where you know that a predicate
--   <tt>P</tt> is satisfied for a specific <tt>a</tt> at compile-time.
module Data.Type.Predicate.Auto

-- | Automatically generate a witness for predicate <tt>p</tt> applied to
--   input <tt>a</tt>.
--   
--   Mostly useful for situations where you know <tt>a</tt> at
--   compile-time, so you can just write <a>auto</a> directly in your
--   source code. The choice is intended to mirror the <tt>auto</tt>
--   keyword in languages like Idris.
--   
--   Very close in nature to the <tt>Known</tt> typeclass in the
--   <i>type-combinators</i> library.
--   
--   Admittedly this interface is a bit clunky and ad-hoc; at this point
--   you can just try writing <a>auto</a> in your code and praying that it
--   works. You always have the option, of course, to just manually write
--   proofs. If you have any inference rules to suggest, feel free to
--   submit a PR!
--   
--   An important limitation of <a>Auto</a> is the Haskell type system
--   prevents "either-or" constraints; this could potentially be
--   implemented using compiler plugins.
--   
--   One consequence of this is that it is impossible to automatically
--   derive <tt><a>Any</a> f p</tt> and <tt><a>Not</a> (<a>All</a> f
--   p)</tt>.
--   
--   For these, the compiler needs help; you can use <a>autoAny</a> and
--   <a>autoNotAll</a> for these situations.
class Auto (p :: Predicate k) (a :: k)

-- | Have the compiler generate a witness for <tt>p @@ a</tt>.
--   
--   Must be called using type application syntax:
--   
--   <pre>
--   <a>auto</a> <tt>_ </tt>p @a
--   </pre>
auto :: Auto p a => p @@ a

-- | A version of <a>auto</a> that "just works" with type inference, if the
--   predicate is a type constructor.
autoTC :: forall t a. Auto (TyPred t) a => t a

-- | An <tt><a>AutoNot</a> p a</tt> constraint means that <tt>p @@ a</tt>
--   can be proven to not be true at compiletime.
type AutoNot (p :: Predicate k) = Auto (Not p)

-- | Disprove <tt>p @@ a</tt> at compiletime.
--   
--   <pre>
--   <a>autoNot</a> @_ @p @a :: <a>Not</a> p <a>@@</a> a
--   </pre>
autoNot :: forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a

-- | Helper function to generate an <tt><a>Any</a> f p</tt> if you can pick
--   out a specific <tt>a</tt> in <tt>as</tt> where the predicate is
--   provable at compile-time.
--   
--   This is used to get around a fundamental limitation of <a>Auto</a> as
--   a Haskell typeclass.
autoAny :: forall f p as a. Auto p a => Elem f as a -> Any f p @@ as

-- | Helper function to generate a <tt><a>Not</a> (<a>All</a> f p)</tt> if
--   you can pick out a specific <tt>a</tt> in <tt>as</tt> where the
--   predicate is disprovable at compile-time.
--   
--   This is used to get around a fundamental limitation of <a>Auto</a> as
--   a Haskell typeclass.
autoNotAll :: forall p f as a. (AutoNot p a, SingI as) => Elem f as a -> Not (All f p) @@ as

-- | Helper "predicate transformer" that gives you an instant <a>auto</a>
--   for any <a>Provable</a> instance.
--   
--   For example, say you have predicate <tt>P</tt> that you know is
--   <a>Provable</a>, and you wish to generate a <tt>P @@ x</tt>, for some
--   specific <tt>x</tt> you know at compile-time. You can use:
--   
--   <pre>
--   <a>auto</a> @_ @(<a>AutoProvable</a> P) @x
--   </pre>
--   
--   to obtain a <tt>P @@ x</tt>.
--   
--   <a>AutoProvable</a> is essentially the identity function.
data AutoProvable :: Predicate k -> Predicate k

-- | Typeclass representing <a>Elem</a>s pointing to an <tt>a :: k</tt>
--   that can be generated automatically from type-level collection <tt>as
--   :: f k</tt>.
--   
--   If GHC knows both the type-level collection and the element you want
--   to find at compile-time, this instance should allow it to find it.
--   
--   Used to help in the instance of <a>Auto</a> for the <a>In</a>
--   predicate.
--   
--   Example usage:
--   
--   <pre>
--   <a>autoElem</a> :: <a>Index</a> '[1,6,2,3] 2
--   -- IS (IS IZ)        -- third spot
--   </pre>
--   
--   And when used with <a>Auto</a>:
--   
--   <pre>
--   <a>auto</a> @_ @(<a>In</a> [] '[1,6,2,3]) @2
--   -- IS (IS IZ)
--   </pre>
class AutoElem f (as :: f k) (a :: k)

-- | Generate the <a>Elem</a> pointing to the <tt>a :: </tt> in a
--   type-level collection <tt>as :: f k</tt>.
autoElem :: AutoElem f as a => Elem f as a

-- | Helper class for deriving <a>Auto</a> instances for <a>All</a>
--   predicates; each <a>Universe</a> instance is expected to implement
--   these if possible, to get free <a>Auto</a> instaces for their
--   <a>All</a> predicates.
--   
--   Also helps for <a>Not</a> <a>Any</a> predicates and <a>Not</a>
--   <a>Found</a> <a>AnyMatch</a> predicates.
class AutoAll f (p :: Predicate k) (as :: f k)

-- | Generate an <a>All</a> for a given predicate over all items in
--   <tt>as</tt>.
autoAll :: AutoAll f p as => All f p @@ as
instance forall j k (p :: Data.Type.Predicate.Predicate j) (f :: k Data.Singletons.~> j) (a :: k). Data.Type.Predicate.Auto.AutoNot p (f Data.Singletons.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Not (Data.Type.Predicate.PMap f p)) a
instance forall k (p :: Data.Type.Predicate.Predicate k). Data.Type.Predicate.Auto.AutoAll [] p '[]
instance forall a1 (p :: Data.Type.Predicate.Predicate a1) (a2 :: a1) (as :: [a1]). (Data.Type.Predicate.Auto.Auto p a2, Data.Type.Predicate.Auto.AutoAll [] p as) => Data.Type.Predicate.Auto.AutoAll [] p (a2 : as)
instance forall k (p :: Data.Type.Predicate.Predicate k). Data.Type.Predicate.Auto.AutoAll GHC.Maybe.Maybe p 'GHC.Maybe.Nothing
instance forall a1 (p :: Data.Type.Predicate.Predicate a1) (a2 :: a1). Data.Type.Predicate.Auto.Auto p a2 => Data.Type.Predicate.Auto.AutoAll GHC.Maybe.Maybe p ('GHC.Maybe.Just a2)
instance forall k j (p :: Data.Type.Predicate.Predicate k) (e :: j). Data.Type.Predicate.Auto.AutoAll (Data.Either.Either j) p ('Data.Either.Left e)
instance forall b (p :: Data.Type.Predicate.Predicate b) (a :: b) j. Data.Type.Predicate.Auto.Auto p a => Data.Type.Predicate.Auto.AutoAll (Data.Either.Either j) p ('Data.Either.Right a)
instance forall a1 (p :: Data.Type.Predicate.Predicate a1) (a2 :: a1) (as :: [a1]). (Data.Type.Predicate.Auto.Auto p a2, Data.Type.Predicate.Auto.AutoAll [] p as) => Data.Type.Predicate.Auto.AutoAll GHC.Base.NonEmpty p (a2 'GHC.Base.:| as)
instance forall k (p :: Data.Type.Predicate.Predicate k) (a :: k) j (w :: j). Data.Type.Predicate.Auto.Auto p a => Data.Type.Predicate.Auto.AutoAll ((,) j) p '(w, a)
instance forall a1 (p :: Data.Type.Predicate.Predicate a1) (a2 :: a1). Data.Type.Predicate.Auto.Auto p a2 => Data.Type.Predicate.Auto.AutoAll Data.Functor.Identity.Identity p ('Data.Functor.Identity.Identity a2)
instance forall k (f :: * -> *) (p :: Data.Type.Predicate.Predicate k) (as :: f k). Data.Type.Predicate.Auto.AutoAll f p as => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.All f p) as
instance forall k (f :: * -> *) (as :: f k) (p :: Data.Type.Predicate.Predicate k). (Data.Singletons.SingI as, Data.Type.Predicate.Auto.AutoAll f (Data.Type.Predicate.Not p) as) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Not (Data.Type.Universe.Any f p)) as
instance forall k v (f :: * -> *) (as :: f k) (p :: Data.Type.Predicate.Param.ParamPred k v). (Data.Singletons.SingI as, Data.Type.Predicate.Auto.AutoAll f (Data.Type.Predicate.Not (Data.Type.Predicate.Param.Found p)) as) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Not (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.AnyMatch f p))) as
instance forall k (a :: k) (as :: [k]). Data.Type.Predicate.Auto.AutoElem [] (a : as) a
instance forall k (as :: [k]) (a :: k) (b :: k). Data.Type.Predicate.Auto.AutoElem [] as a => Data.Type.Predicate.Auto.AutoElem [] (b : as) a
instance forall k (a :: k). Data.Type.Predicate.Auto.AutoElem GHC.Maybe.Maybe ('GHC.Maybe.Just a) a
instance forall k j (a :: k). Data.Type.Predicate.Auto.AutoElem (Data.Either.Either j) ('Data.Either.Right a) a
instance forall k (a :: k) (as :: [k]). Data.Type.Predicate.Auto.AutoElem GHC.Base.NonEmpty (a 'GHC.Base.:| as) a
instance forall k (as :: [k]) (a :: k) (b :: k). Data.Type.Predicate.Auto.AutoElem [] as a => Data.Type.Predicate.Auto.AutoElem GHC.Base.NonEmpty (b 'GHC.Base.:| as) a
instance forall k j (w :: j) (a :: k). Data.Type.Predicate.Auto.AutoElem ((,) j) '(w, a) a
instance forall k (a :: k). Data.Type.Predicate.Auto.AutoElem Data.Functor.Identity.Identity ('Data.Functor.Identity.Identity a) a
instance forall k (f :: * -> *) (as :: f k) (a :: k). Data.Type.Predicate.Auto.AutoElem f as a => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.In f as) a
instance forall k (p :: k Data.Singletons.~> *) (a :: k). (Data.Type.Predicate.Provable p, Data.Singletons.SingI a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Auto.AutoProvable p) a
instance forall k (a :: k). Data.Singletons.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Predicate.Evident a
instance forall k (a :: k). Data.Singletons.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Not Data.Type.Predicate.Impossible) a
instance forall k (a :: k). Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.EqualTo a) a
instance forall k (p :: Data.Type.Predicate.Predicate k) (a :: k) (q :: Data.Type.Predicate.Predicate k). (Data.Type.Predicate.Auto.Auto p a, Data.Type.Predicate.Auto.Auto q a) => Data.Type.Predicate.Auto.Auto (p Data.Type.Predicate.Logic.&&& q) a
instance forall k (q :: Data.Type.Predicate.Predicate k) (a :: k) (p :: Data.Type.Predicate.Predicate k). Data.Type.Predicate.Auto.Auto q a => Data.Type.Predicate.Auto.Auto (p Data.Type.Predicate.Logic.==> q) a
instance forall k (a :: k) (as :: [k]). Data.Singletons.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull []) (a : as)
instance forall k (a :: k). Data.Singletons.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Universe.IsJust ('GHC.Maybe.Just a)
instance forall k j (a :: k). Data.Singletons.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Universe.IsRight ('Data.Either.Right a)
instance forall k (a :: k) (as :: [k]). Data.Singletons.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull GHC.Base.NonEmpty) (a 'GHC.Base.:| as)
instance forall k (a :: k) j (w :: j). Data.Singletons.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull ((,) j)) '(w, a)
instance forall k (a :: k). Data.Singletons.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull Data.Functor.Identity.Identity) ('Data.Functor.Identity.Identity a)
instance forall j v k (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.~> j) (a :: k). Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.Found p) (f Data.Singletons.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.PPMap f p)) a
instance forall j v k (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.~> j) (a :: k). Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.NotFound p) (f Data.Singletons.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.NotFound (Data.Type.Predicate.Param.PPMap f p)) a
instance forall j k (p :: Data.Type.Predicate.Predicate j) (f :: k Data.Singletons.~> j) (a :: k). Data.Type.Predicate.Auto.Auto p (f Data.Singletons.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.PMap f p) a
instance forall u (as :: [u]). Data.Singletons.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Vinyl.Core.Rec Data.Singletons.WrappedSing)) as
instance forall k (as :: GHC.Maybe.Maybe k). Data.Singletons.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe Data.Singletons.WrappedSing)) as
instance forall k (as :: GHC.Base.NonEmpty k). Data.Singletons.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec Data.Singletons.WrappedSing)) as
instance forall j k (as :: Data.Either.Either j k). Data.Singletons.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither Data.Singletons.WrappedSing)) as
instance forall j k (as :: (j, k)). Data.Singletons.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup Data.Singletons.WrappedSing)) as
instance forall k (as :: Data.Functor.Identity.Identity k). Data.Singletons.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity Data.Singletons.WrappedSing)) as
instance forall u (as :: [u]) (p :: u Data.Singletons.~> *). (Data.Singletons.SingI as, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Vinyl.Core.Rec (Data.Type.Predicate.Wit p))) as
instance forall k (as :: GHC.Maybe.Maybe k) (p :: k Data.Singletons.~> *). (Data.Singletons.SingI as, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe (Data.Type.Predicate.Wit p))) as
instance forall k (as :: GHC.Base.NonEmpty k) (p :: k Data.Singletons.~> *). (Data.Singletons.SingI as, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec (Data.Type.Predicate.Wit p))) as
instance forall j k (as :: Data.Either.Either j k) (p :: k Data.Singletons.~> *). (Data.Singletons.SingI as, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither (Data.Type.Predicate.Wit p))) as
instance forall j k (as :: (j, k)) (p :: k Data.Singletons.~> *). (Data.Singletons.SingI as, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup (Data.Type.Predicate.Wit p))) as
instance forall k (as :: Data.Functor.Identity.Identity k) (p :: k Data.Singletons.~> *). (Data.Singletons.SingI as, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity (Data.Type.Predicate.Wit p))) as


-- | Represent a decidable subset of a type-level collection.
module Data.Type.Universe.Subset

-- | A <tt><a>Subset</a> f p</tt> is a predicate that some decidable subset
--   of an input <tt>as</tt> is true.
data Subset f :: (k ~> Type) -> (f k ~> Type)

-- | A <tt><a>WitSubset</a> f p </tt><tt> as</tt> describes a
--   <i>decidable</i> subset of type-level collection <tt>as</tt>.
newtype WitSubset f p (as :: f k)
WitSubset :: (forall a. Elem f as a -> Decision (p @@ a)) -> WitSubset f p (as :: f k)
[runWitSubset] :: WitSubset f p (as :: f k) -> forall a. Elem f as a -> Decision (p @@ a)

-- | Create a <a>Subset</a> from a predicate.
makeSubset :: forall f k p (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Subset f p @@ as

-- | Subset intersection
intersection :: forall f p q. () => (Subset f p &&& Subset f q) --> Subset f (p &&& q)

-- | Subset union (left-biased)
union :: forall f p q. () => (Subset f p &&& Subset f q) --> Subset f (p ||| q)

-- | Symmetric subset difference
symDiff :: forall f p q. () => (Subset f p &&& Subset f q) --> Subset f (p ^^^ q)

-- | Combine two subsets based on a decision function
mergeSubset :: forall f k p q r (as :: f k). () => (forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) -> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as

-- | Combine two subsets based on a decision function
imergeSubset :: forall f k p q r (as :: f k). () => (forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) -> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as

-- | Map a bidirectional implication over a subset described by that
--   implication.
--   
--   Implication needs to be bidirectional, or otherwise we can't produce a
--   <i>decidable</i> subset as a result.
mapSubset :: Universe f => (p --> q) -> (q --> p) -> Subset f p --> Subset f q

-- | <a>mapSubset</a>, but providing an <a>Elem</a>.
imapSubset :: (forall a. Elem f as a -> (p @@ a) -> q @@ a) -> (forall a. Elem f as a -> (q @@ a) -> p @@ a) -> (Subset f p @@ as) -> Subset f q @@ as

-- | Turn a <a>Subset</a> into a list (or any <a>Alternative</a>) of
--   satisfied predicates.
--   
--   List is meant to include no duplicates.
subsetToList :: forall f p t. (Universe f, Alternative t) => (Subset f p --># Any f p) t

-- | Restrict a <a>Subset</a> to a single (arbitrary) member, or fail if
--   none exists.
subsetToAny :: forall f p. Universe f => Subset f p -?> Any f p

-- | Test if a subset is equal to the entire original collection
subsetToAll :: forall f p. Universe f => Subset f p -?> All f p

-- | Test if a subset is empty.
subsetToNone :: forall f p. Universe f => Subset f p -?> None f p

-- | Construct an empty subset.
emptySubset :: forall f as. (Universe f, SingI as) => Subset f Impossible @@ as

-- | Construct a full subset
fullSubset :: forall f as. (Universe f, SingI as) => Subset f Evident @@ as
instance forall k (f :: * -> *) (p :: k Data.Singletons.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Decidable (Data.Type.Universe.Subset.Subset f p)
instance forall k (f :: * -> *) (p :: k Data.Singletons.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Provable (Data.Type.Universe.Subset.Subset f p)