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


-- | 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 '-&gt;' 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>
type Evident = (TyPred Sing :: 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.Internal.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.Internal.SingI as) => Data.Type.Predicate.Decidable (Data.Type.Predicate.In GHC.Maybe.Maybe as)
instance forall j k (as :: Data.Either.Either j k). (Data.Singletons.Decide.SDecide k, Data.Singletons.Internal.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.Internal.SingI as) => Data.Type.Predicate.Decidable (Data.Type.Predicate.In GHC.Base.NonEmpty as)
instance forall j k (as :: (j, k)). (Data.Singletons.Decide.SDecide k, Data.Singletons.Internal.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.Internal.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.Internal.~> *). 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.Internal.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.Vinyl.Core.Rec Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup Data.Singletons.Internal.Sing))
instance forall k1 j (p :: j Data.Singletons.Internal.~> *) (f :: k1 Data.Singletons.Internal.~> j). (Data.Type.Predicate.Decidable p, Data.Singletons.Internal.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.Vinyl.Core.Rec Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither Data.Singletons.Internal.Sing))
instance Data.Type.Predicate.Provable (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup Data.Singletons.Internal.Sing))
instance forall k1 j (p :: j Data.Singletons.Internal.~> *) (f :: k1 Data.Singletons.Internal.~> j). (Data.Type.Predicate.Provable p, Data.Singletons.Internal.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>
type Evident = (TyPred Sing :: 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.Internal.~> *) (q :: k1 Data.Singletons.Internal.~> *). (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.Internal.~> *) (q :: k1 Data.Singletons.Internal.~> *). (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.Internal.~> *) (q :: k1 Data.Singletons.Internal.~> *). (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) :: forall k. () => [k] -> k -> Type
[IZ] :: forall k (a :: [k]) (b :: k) (as :: [k]). () => Index (b : as) b
[IS] :: forall k (a :: [k]) (b :: k) (bs :: [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) :: forall k. () => Maybe k -> k -> Type
[IJust] :: forall k (a :: Maybe 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) :: forall j k. () => Either j k -> k -> Type
[IRight] :: forall j k (a :: Either j k) (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) :: forall k. () => NonEmpty k -> k -> Type
[NEHead] :: forall k (a :: NonEmpty k) (b :: k) (as :: [k]). () => NEIndex (b :| as) b
[NETail] :: forall k (a :: NonEmpty k) (b :: k) (as :: [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) :: forall j k. () => (j, k) -> k -> Type
[ISnd] :: forall j k (a :: (j, k)) (b :: k) (a1 :: j). () => ISnd ((,) a1 b) b

-- | Trivially witness the item held in an <a>Identity</a>.
data IIdentity (a :: Identity k) (b :: k) :: forall k. () => Identity k -> k -> Type
[IId] :: forall k (a :: Identity 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
[runWitAll] :: WitAll f p -> 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.Internal.~> *). (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.Internal.~> *) (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.Internal.~> *). (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.Internal.~> *). (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.Internal.~> *). (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
[runWitAll] :: WitAll f p -> 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 '-&gt;' 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 u k1 v (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 u k1 v (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 k (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.Internal.~> j). (Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found p), Data.Singletons.Internal.SingI f) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.PPMap f p))
instance forall j v k (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.Internal.~> j). (Data.Type.Predicate.Provable (Data.Type.Predicate.Param.Found p), Data.Singletons.Internal.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

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

-- | 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
instance forall k j (p :: Data.Type.Predicate.Predicate j) (f :: k Data.Singletons.Internal.~> j) (a :: k). Data.Type.Predicate.Auto.AutoNot p (f Data.Singletons.Internal.@@ 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.Internal.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 v k (f :: * -> *) (as :: f k) (p :: Data.Type.Predicate.Param.ParamPred k v). (Data.Singletons.Internal.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.Internal.~> *) (a :: k). (Data.Type.Predicate.Provable p, Data.Singletons.Internal.SingI a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Auto.AutoProvable p) a
instance forall k (a :: k). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Predicate.Evident a
instance forall k (a :: k). Data.Singletons.Internal.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.Internal.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull []) (a : as)
instance forall k (a :: k). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Universe.IsJust ('GHC.Maybe.Just a)
instance forall j k (a :: k). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Universe.IsRight ('Data.Either.Right a)
instance forall k (a :: k) (as :: [k]). Data.Singletons.Internal.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.Internal.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull ((,) j)) '(w, a)
instance forall k (a :: k). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull Data.Functor.Identity.Identity) ('Data.Functor.Identity.Identity a)
instance forall k j v (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.Internal.~> j) (a :: k). Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.Found p) (f Data.Singletons.Internal.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.PPMap f p)) a
instance forall k j v (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.Internal.~> j) (a :: k). Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.NotFound p) (f Data.Singletons.Internal.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.NotFound (Data.Type.Predicate.Param.PPMap f p)) a
instance forall k j (p :: Data.Type.Predicate.Predicate j) (f :: k Data.Singletons.Internal.~> j) (a :: k). Data.Type.Predicate.Auto.Auto p (f Data.Singletons.Internal.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.PMap f p) a
instance forall u (as :: [u]). Data.Singletons.Internal.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Vinyl.Core.Rec Data.Singletons.Internal.Sing)) as
instance forall k (as :: GHC.Maybe.Maybe k). Data.Singletons.Internal.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PMaybe Data.Singletons.Internal.Sing)) as
instance forall k (as :: GHC.Base.NonEmpty k). Data.Singletons.Internal.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.NERec Data.Singletons.Internal.Sing)) as
instance forall j k (as :: Data.Either.Either j k). Data.Singletons.Internal.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PEither Data.Singletons.Internal.Sing)) as
instance forall j k (as :: (j, k)). Data.Singletons.Internal.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PTup Data.Singletons.Internal.Sing)) as
instance forall k (as :: Data.Functor.Identity.Identity k). Data.Singletons.Internal.SingI as => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.TyPred (Data.Type.Functor.Product.PIdentity Data.Singletons.Internal.Sing)) 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
[runWitSubset] :: WitSubset f p -> 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.Internal.~> *). (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.Internal.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Provable (Data.Type.Universe.Subset.Subset f p)