-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Combinators for manipulating dependently-typed predicates.
--
-- Please see the README on GitHub at
-- https://github.com/mstksg/decidable#readme
@package decidable
@version 0.1.1.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 P ::
-- Predicate k is true/satisfied by input x :: k if
-- there exists a value of type P @@ x, and that it
-- false/disproved if such a value cannot exist. (Where @@ is
-- Apply, the singleton library's type-level function application
-- for mathcable functions)
--
-- See Provable and Decidable for more information on how
-- to use, prove and decide these predicates.
--
-- The kind k ~> Type 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:
--
--
-- - Using the predicate combinators and predicate transformers in this
-- library and the singletons library, which let you construct
-- pre-made predicates and sometimes create predicates from other
-- predicates.
-- - Manually creating a data type that acts as a matchable
-- predicate.
--
--
-- For an example of the latter, we can create the "not p" predicate,
-- which takes a predicate p as input and returns the negation
-- of the predicate:
--
--
-- -- First, create the data type with the kind signature you want
-- data Not :: Predicate k -> Predicate k
--
-- -- Then, write the Apply instance, to specify the type of the
-- -- witnesses of that predicate
-- instance Apply (Not p) a = (p @@ a) -> Void
--
--
-- See the source of Data.Type.Predicate and
-- Data.Type.Predicate.Logic for simple examples of hand-made
-- predicates. For example, we have the always-true predicate
-- Evident:
--
--
-- data Evident :: Predicate k
-- instance Apply Evident a = Sing a
--
--
-- And the "and" predicate combinator:
--
--
-- data (&&&) :: Predicate k -> Predicate k -> Predicate k
-- instance Apply (p &&& q) a = (p @@ a, q @@ a)
--
--
-- Typically it is recommended to create predicates from the supplied
-- predicate combinators (TyPred can be used for any type
-- constructor to turn it into a predicate, for instance) whenever
-- possible.
type Predicate k = k ~> Type
-- | A Wit p a is a value of type p @@ a --- that
-- is, it is a proof or witness that p is satisfied for
-- a.
--
-- It essentially turns a k ~> Type ("matchable"
-- Predicate k) /back into/ a k ->
-- Type predicate.
newtype Wit p a
Wit :: p @@ a -> Wit p a
[getWit] :: Wit p a -> p @@ a
-- | Convert a normal '->' type constructor into a Predicate.
--
--
-- TyPred :: (k -> Type) -> Predicate k
--
type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)
-- | The always-true predicate.
--
--
-- Evident :: Predicate k
--
type Evident = (TyPred Sing :: Predicate k)
-- | EqualTo a is a predicate that the input is equal to
-- a.
type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)
-- | Convert a tradtional k ~> Bool predicate into a
-- Predicate.
--
--
-- BoolPred :: (k ~> Bool) -> Predicate k
--
type BoolPred (p :: k ~> Bool) = (EqualTo 'True .@#@$$$ p :: Predicate k)
-- | The always-false predicate
--
-- Could also be defined as ConstSym1 Void, but this
-- defintion gives us a free Decidable instance.
type Impossible = (Not Evident :: Predicate k)
-- | Pre-compose a function to a predicate
--
--
-- PMap :: (k ~> j) -> Predicate j -> Predicate k
--
type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)
-- | Not p is the predicate that p is not true.
data Not :: Predicate k -> Predicate k
-- | Decide Not p based on decisions of p.
decideNot :: forall p a. () => Decision (p @@ a) -> Decision (Not p @@ a)
-- | A proving function for predicate p. See Provable for
-- more information.
type Prove p = forall a. Sing a -> p @@ a
-- | We say that p implies q (p --> q)
-- if, given p a, we can always prove q @@ a.
type p --> q = forall a. Sing a -> p @@ a -> q @@ a
-- | This is implication -->#, but only in a specific context
-- h.
type ( p --># q ) h = forall a. Sing a -> p @@ a -> h (q @@ a)
-- | A typeclass for provable predicates (constructivist tautologies).
--
-- A predicate is provable if, given any input a, you can
-- generate a proof of p @@ a. Essentially, it means that a
-- predicate is "always true".
--
-- This typeclass associates a canonical proof function for every
-- provable predicate.
--
-- It confers two main advatnages:
--
--
-- - The proof function for every predicate is available via the same
-- name
-- - We can write Provable instances for polymorphic predicate
-- transformers (predicates parameterized on other predicates) easily, by
-- refering to Provable instances of the transformed
-- predicates.
--
class Provable p
-- | The canonical proving function for predicate p.
--
-- Note that prove is ambiguously typed, so you always need
-- to call by specifying the predicate you want to prove using
-- TypeApplications syntax:
--
--
-- prove @MyPredicate
--
prove :: Provable p => Prove p
-- | Disprovable p is a constraint that p can be
-- disproven.
type Disprovable p = Provable (Not p)
-- | The deciding/disproving function for Disprovable p.
--
-- Must be called by applying the Predicate to disprove:
--
--
-- disprove @p
--
disprove :: forall p. Disprovable p => Prove (Not p)
-- | If T :: k -> Type is a type constructor, then
-- ProvableTC T is a constraint that T is
-- "decidable", in that you have a canonical function:
--
--
-- proveTC :: Sing a -> T a
--
--
-- Is essentially Provable, except with type constructors
-- k -> Type instead of matchable type-level functions
-- (that are k ~> Type).
type ProvableTC p = Provable (TyPred p)
-- | The canonical proving function for DecidableTC t.
proveTC :: forall t a. ProvableTC t => Sing a -> t a
-- | Implicatons p --> q can be lifted "through" a
-- TFunctor into an f p --> f q.
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 p. See Decidable for
-- more information.
type Decide p = forall a. Sing a -> Decision (p @@ a)
-- | Like implication -->, but knowing p @@ a can only
-- let us decidably prove q a is true or false.
type p -?> q = forall a. Sing a -> p @@ a -> Decision (q @@ a)
-- | Like -?>, but only in a specific context h.
type ( p -?># q ) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a))
-- | A typeclass for decidable predicates.
--
-- A predicate is decidable if, given any input a, you can
-- either prove or disprove p @@ a. A Decision (p @@
-- a) is a data type that has a branch p @@ a and
-- Refuted (p @@ a).
--
-- This typeclass associates a canonical decision function for every
-- decidable predicate.
--
-- It confers two main advatnages:
--
--
-- - The decision function for every predicate is available via the
-- same name
-- - We can write Decidable instances for polymorphic predicate
-- transformers (predicates parameterized on other predicates) easily, by
-- refering to Decidable instances of the transformed
-- predicates.
--
class Decidable p
-- | The canonical decision function for predicate p.
--
-- Note that decide is ambiguously typed, so you always
-- need to call by specifying the predicate you want to prove using
-- TypeApplications syntax:
--
--
-- decide @MyPredicate
--
decide :: Decidable p => Decide p
-- | The canonical decision function for predicate p.
--
-- Note that decide is ambiguously typed, so you always
-- need to call by specifying the predicate you want to prove using
-- TypeApplications syntax:
--
--
-- decide @MyPredicate
--
decide :: (Decidable p, Provable p) => Decide p
-- | If T :: k -> Type is a type constructor, then
-- DecidableTC T is a constraint that T is
-- "decidable", in that you have a canonical function:
--
--
-- decideTC :: Sing a -> Decision (T a)
--
--
-- Is essentially Decidable, except with type constructors
-- k -> Type instead of matchable type-level functions
-- (that are k ~> Type).
type DecidableTC p = Decidable (TyPred p)
-- | The canonical deciding function for DecidableTC t.
decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)
-- | Implicatons p -?> q can be lifted "through" a
-- DFunctor into an f p -?> f q.
class DFunctor f
dmap :: forall p q. DFunctor f => (p -?> q) -> (f p -?> f q)
-- | A Decision about a type a is either a proof of
-- existence or a proof that a cannot exist.
data Decision a
-- | Witness for a
Proved :: a -> Decision a
-- | Proof that no a exists
Disproved :: Refuted a -> Decision a
-- | Flip the contents of a decision. Turn a proof of a into a
-- disproof of not-a.
--
-- Note that this is not reversible in general in Haskell. See
-- doubleNegation for a situation where it is.
flipDecision :: Decision a -> Decision (Refuted a)
-- | Map over the value inside a Decision.
mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b
-- | Converts a Decision to a Maybe. Drop the witness of
-- disproof of a, returning Just if Proved (with
-- the proof) and Nothing if Disproved.
forgetDisproof :: Decision a -> Maybe a
-- | Drop the witness of proof of a, returning Nothing if
-- Proved and Just if Disproved (with the disproof).
forgetProof :: Decision a -> Maybe (Refuted a)
-- | Boolean test if a Decision is Proved.
isProved :: Decision a -> Bool
-- | Boolean test if a Decision is Disproved.
isDisproved :: Decision a -> Bool
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 forall k1 b6989586621679419814 (f :: b6989586621679419814 Data.Singletons.Internal.~> *) (g :: Data.Singletons.Internal.TyFun k1 b6989586621679419814 -> *). (Data.Type.Predicate.Decidable f, Data.Singletons.Internal.SingI g) => Data.Type.Predicate.Decidable (f Data.Singletons.Prelude.Base..@#@$$$ g)
instance Data.Type.Predicate.Provable Data.Type.Predicate.Evident
instance forall k1 b6989586621679419814 (f :: b6989586621679419814 Data.Singletons.Internal.~> *) (g :: Data.Singletons.Internal.TyFun k1 b6989586621679419814 -> *). (Data.Type.Predicate.Provable f, Data.Singletons.Internal.SingI g) => Data.Type.Predicate.Provable (f Data.Singletons.Prelude.Base..@#@$$$ g)
-- | Logical and algebraic connectives for predicates, as well as common
-- logical combinators.
module Data.Type.Predicate.Logic
-- | The always-true predicate.
--
--
-- Evident :: Predicate k
--
type Evident = (TyPred Sing :: Predicate k)
-- | The always-false predicate
--
-- Could also be defined as ConstSym1 Void, but this
-- defintion gives us a free Decidable instance.
type Impossible = (Not Evident :: Predicate k)
-- | Not p is the predicate that p is not true.
data Not :: Predicate k -> Predicate k
-- | Decide Not p based on decisions of p.
decideNot :: forall p a. () => Decision (p @@ a) -> Decision (Not p @@ a)
-- | p &&& q is a predicate that both
-- p and q are true.
data (&&&) :: Predicate k -> Predicate k -> Predicate k
-- | Decide p &&& q based on decisions of
-- p and q.
decideAnd :: forall p q a. () => Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
-- | p ||| q is a predicate that either p and
-- q are true.
data (|||) :: Predicate k -> Predicate k -> Predicate k
-- | Decide p ||| q based on decisions of p and
-- q.
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
-- | p ^^^ q is a predicate that either p and
-- q are true, but not both.
type p ^^^ q = (p &&& Not q) ||| (Not p &&& q)
-- | Decide p ^^^ q based on decisions of p and
-- q.
decideXor :: forall p q a. () => Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)
-- | p ==> q is true if q is provably true under the
-- condition that p is true.
data (==>) :: Predicate k -> Predicate k -> Predicate k
-- | If q is provable, then so is p ==> q.
--
-- This can be used as an easy plug-in Provable instance for p
-- ==> q if q is Provable:
--
--
-- instance Provable (p ==> MyPred) where
-- prove = proveImplies @MyPred
--
--
-- This instance isn't provided polymorphically because of overlapping
-- instance issues.
proveImplies :: Prove q -> Prove (p ==> q)
-- | Implies p q is a constraint that p ==>
-- q is Provable; that is, you can prove that p
-- implies q.
type Implies p q = Provable (p ==> q)
-- | Two-way implication, or logical equivalence
type p <==> q = p ==> q &&& q ==> p
-- | Equiv p q is a constraint that p <==>
-- q is Provable; that is, you can prove that p is
-- logically equivalent to q.
type Equiv p q = Provable (p <==> q)
-- | Compose two implications.
compImpl :: forall p q r. () => p --> q -> q --> r -> p --> r
-- | From Impossible a, you can prove anything.
-- Essentially a lifted version of absurd.
explosion :: Impossible --> p
-- | Evident can be proven from all predicates.
atom :: p --> Evident
-- | We cannot have both p and Not p.
excludedMiddle :: (p &&& Not p) --> Impossible
-- | Logical double negation. Only possible if p is
-- Decidable.
doubleNegation :: forall p. Decidable p => Not (Not p) --> p
-- | If only this worked, but darn overlapping instances. Same for p ==>
-- p ||| q and p &&& q ==> p :( q) ==> instance
-- Provable (p &&& Not p ==> Impossible) where prove =
-- excludedMiddle @p
--
-- If p implies q, then not q implies not p.
contrapositive :: (p --> q) -> (Not q --> Not p)
-- | Reverse direction of contrapositive. Only possible if
-- q is Decidable on its own, without the help of
-- p, which makes this much less useful.
contrapositive' :: forall p q. Decidable q => (Not q --> Not p) -> (p --> q)
-- | If p &&& q is true, then so is p.
projAndFst :: (p &&& q) --> p
-- | If p &&& q is true, then so is q.
projAndSnd :: (p &&& q) --> q
-- | If p is true, then so is p ||| q.
injOrLeft :: forall p q. p --> (p ||| q)
-- | If q is true, then so is p ||| q.
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 :: 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)
-- | Combinators for working with type-level predicates, along with
-- typeclasses for canonical proofs and deciding functions.
module Data.Type.Universe
-- | A witness for membership of a given item in a type-level collection
-- | In f as is a predicate that a given input a
-- is a member of collection as.
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 Universe (f :: Type -> Type)
-- | decideAny, but providing an Elem.
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))
-- | decideAll, but providing an Elem.
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))
-- | genAllA, but providing an Elem.
igenAllA :: forall k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h) => (forall a. Elem f as a -> Sing a -> h (p @@ a)) -> (Sing as -> h (All f p @@ as))
-- | Witness an item in a type-level list by providing its index.
data Index :: [k] -> k -> Type
[IZ] :: Index (a : as) a
[IS] :: Index bs a -> Index (b : bs) a
-- | Witness an item in a type-level Maybe by proving the
-- Maybe is Just.
data IsJust :: Maybe k -> k -> Type
[IsJust] :: IsJust ( 'Just a) a
-- | Witness an item in a type-level Either j by proving
-- the Either is Right.
data IsRight :: Either j k -> k -> Type
[IsRight] :: IsRight ( 'Right a) a
-- | Witness an item in a type-level NonEmpty by either indicating
-- that it is the "head", or by providing an index in the "tail".
data NEIndex :: NonEmpty k -> k -> Type
[NEHead] :: NEIndex (a :| as) a
[NETail] :: Index as a -> NEIndex (b :| as) a
-- | Trivially witness an item in the second field of a type-level tuple.
data Snd :: (j, k) -> k -> Type
[Snd] :: Snd '(a, b) b
-- | An All f p is a predicate testing a collection as
-- :: f a for the fact that all items in as satisfy
-- p. Represents the "forall" quantifier over a given universe.
--
-- This is mostly useful for its Decidable, Provable, and
-- TFunctor instances, which lets you lift predicates on
-- p to predicates on All f p.
data All f :: (k ~> Type) -> (f k ~> Type)
-- | A WitAll p as is a witness that the predicate p
-- a is true for all items a in the type-level collection
-- as.
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
-- | An Any f p is a predicate testing a collection as
-- :: f a for the fact that at least one item in as
-- satisfies p. Represents the "exists" quantifier over a given
-- universe.
--
-- This is mostly useful for its Decidable and TFunctor
-- instances, which lets you lift predicates on p to predicates
-- on Any f p.
data Any f :: (k ~> Type) -> (f k ~> Type)
-- | A WitAny p as is a witness that, for at least one item
-- a in the type-level collection as, the predicate
-- p a is true.
data WitAny f :: (k ~> Type) -> f k -> Type
[WitAny] :: Elem f as a -> p @@ a -> WitAny f p as
-- | A None f p is a predicate on a collection as
-- that no a in as satisfies predicate p.
type None f p = (Not (Any f p) :: Predicate (f k))
-- | Predicate that a given as :: f k is empty and has no items in
-- it.
type Null f = (None f Evident :: Predicate (f k))
-- | Predicate that a given as :: f k is not empty, and has at
-- least one item in it.
type NotNull f = (Any f Evident :: Predicate (f k))
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- any item in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
--
-- Essentially tests existential quantification.
decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- all items in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
--
-- Essentially tests universal quantification.
decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)
-- | If p a is true for all values a in as under
-- some (Applicative) context h, then you can create an
-- All p as under that Applicative context h.
--
-- Can be useful with Identity (which is basically unwrapping and
-- wrapping All), or with Maybe (which can express
-- predicates that are either provably true or not provably false).
--
-- In practice, this can be used to iterate and traverse and sequence
-- actions over all "items" in as.
genAllA :: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h) => (forall a. Sing a -> h (p @@ a)) -> (Sing as -> h (All f p @@ as))
-- | If p a is true for all values a in as, then
-- we have All p as. Basically witnesses the definition
-- of All.
genAll :: forall f k (p :: k ~> Type). Universe f => Prove p -> Prove (All f p)
-- | genAll, but providing an Elem.
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)
-- | A foldMap over all items in a collection.
foldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall (a :: k). Sing a -> m) -> Sing as -> m
-- | foldMapUni but with access to the index.
ifoldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall a. Elem f as a -> Sing a -> m) -> Sing as -> m
-- | Extract the item from the container witnessed by the Elem
index :: forall f as a. Universe f => Elem f as a -> Sing as -> Sing a
-- | 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)
data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
instance forall k (as :: [k]) (a :: k). GHC.Show.Show (Data.Type.Universe.Index as a)
instance forall k (as :: GHC.Base.Maybe k) (a :: k). GHC.Show.Show (Data.Type.Universe.IsJust as a)
instance forall j k (as :: Data.Either.Either j k) (a :: k). GHC.Show.Show (Data.Type.Universe.IsRight as a)
instance forall k (as :: GHC.Base.NonEmpty k) (a :: k). GHC.Show.Show (Data.Type.Universe.NEIndex as a)
instance forall j k (as :: (j, k)) (a :: k). GHC.Show.Show (Data.Type.Universe.Snd as a)
instance forall j k (as :: (j, k)). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.Snd as))
instance Data.Type.Universe.Universe ((,) j)
instance forall k (as :: GHC.Base.NonEmpty k). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.NEIndex as))
instance Data.Type.Universe.Universe GHC.Base.NonEmpty
instance forall j k (as :: Data.Either.Either j k). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.IsRight as))
instance Data.Type.Universe.Universe (Data.Either.Either j)
instance forall k (as :: GHC.Base.Maybe k). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.IsJust as))
instance Data.Type.Universe.Universe GHC.Base.Maybe
instance forall k (as :: [k]). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.Index as))
instance Data.Type.Universe.Universe []
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)
-- | Higher-level predicates for quantifying predicates over universes and
-- sets.
module Data.Type.Predicate.Quantification
-- | An Any f p is a predicate testing a collection as
-- :: f a for the fact that at least one item in as
-- satisfies p. Represents the "exists" quantifier over a given
-- universe.
--
-- This is mostly useful for its Decidable and TFunctor
-- instances, which lets you lift predicates on p to predicates
-- on Any f p.
data Any f :: (k ~> Type) -> (f k ~> Type)
-- | A WitAny p as is a witness that, for at least one item
-- a in the type-level collection as, the predicate
-- p a is true.
data WitAny f :: (k ~> Type) -> f k -> Type
[WitAny] :: Elem f as a -> p @@ a -> WitAny f p as
-- | A None f p is a predicate on a collection as
-- that no a in as satisfies predicate p.
type None f p = (Not (Any f p) :: Predicate (f k))
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- any item in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
--
-- Essentially tests existential quantification.
decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)
-- | decideAny, but providing an Elem.
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 p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- no item in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
decideNone :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (None f p)
-- | decideNone, but providing an Elem.
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 a s.t. p a, and if p
-- implies q, then there must exist an a s.t. q
-- a.
entailAny :: forall f p q. Universe f => (p --> q) -> (Any f p --> Any f q)
-- | entailAny, but providing an Elem.
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 p implies q under some context h, and if
-- there exists some a such that p a, then there must
-- exist some a such that p q under that context
-- h.
--
-- h might be something like, say, Maybe, to give
-- predicate that is either provably true or unprovably false.
--
-- Note that it is not possible to do this with p a ->
-- Decision (q a). This is if the p a ->
-- Decision (q a) implication is false, there it doesn't mean
-- that there is no a such that q a,
-- necessarily. There could have been an a where p does
-- not hold, but q does.
entailAnyF :: forall f p q h. (Universe f, Functor h) => (p --># q) h -> (Any f p --># Any f q) h
-- | entailAnyF, but providing an Elem.
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 All f p is a predicate testing a collection as
-- :: f a for the fact that all items in as satisfy
-- p. Represents the "forall" quantifier over a given universe.
--
-- This is mostly useful for its Decidable, Provable, and
-- TFunctor instances, which lets you lift predicates on
-- p to predicates on All f p.
data All f :: (k ~> Type) -> (f k ~> Type)
-- | A WitAll p as is a witness that the predicate p
-- a is true for all items a in the type-level collection
-- as.
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
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- all items in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
--
-- Essentially tests universal quantification.
decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)
-- | decideAll, but providing an Elem.
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 a we have p a, and if p implies
-- q, then for all a we must also have p a.
entailAll :: forall f p q. Universe f => (p --> q) -> (All f p --> All f q)
-- | entailAll, but providing an Elem.
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 p implies q under some context h, and if
-- we have p a for all a, then we must have q
-- a for all a under context h.
entailAllF :: forall f p q h. (Universe f, Applicative h) => (p --># q) h -> (All f p --># All f q) h
-- | entailAllF, but providing an Elem.
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 p a for all a, and p a can be
-- used to test for q a, then we can test all as for
-- q a.
decideEntailAll :: forall f p q. Universe f => p -?> q -> All f p -?> All f q
-- | entailAllF, but providing an Elem.
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)
-- | Manipulate "parameterized predicates". See ParamPred and
-- Found for more information.
module Data.Type.Predicate.Param
-- | A parameterized predicate. See Found for more information.
type ParamPred k v = k -> Predicate v
-- | Flip the arguments of a ParamPred.
data FlipPP :: ParamPred v k -> ParamPred k v
-- | Promote a Predicate v to a ParamPred k
-- v, ignoring the k input.
data ConstPP :: Predicate v -> ParamPred k v
-- | Pre-compose a function to a ParamPred. Is essentially
-- flip (.), but unfortunately defunctionalization
-- doesn't work too well with that definition.
data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v
-- | A ParamPred (f k) k. Parameterized on an as :: f
-- k, returns a predicate that is true if there exists any a ::
-- k in as.
--
-- Essentially NotNull.
type InP f = (ElemSym1 f :: ParamPred (f k) k)
-- | AnyMatch f takes a parmaeterized predicate on
-- k (testing for a v) and turns it into a
-- parameterized predicate on f k (testing for a v). It
-- "lifts" the domain into f.
--
-- An AnyMatch f p as is a predicate taking an argument
-- a and testing if p a :: Predicate k is
-- satisfied for any item in as :: f k.
--
-- A ParamPred k v tests if a k can create some
-- v. The resulting ParamPred (f k) v tests if
-- any k in f k can create some v.
data AnyMatch f :: ParamPred k v -> ParamPred (f k) v
-- | Convert a parameterized predicate into a predicate on the parameter.
--
-- A Found p is a predicate on p :: ParamPred
-- k v that tests a k for the fact that there exists a
-- v where ParamPred k v is satisfied.
--
-- Intended as the basic interface for ParamPred, since it turns a
-- ParamPred into a normal Predicate, which can have
-- Decidable and Provable instances.
--
-- For some context, an instance of Provable (Found
-- P), where P :: ParamPred k v, means that for any
-- input x :: k, we can always find a y :: v such that
-- we have P x y.
--
-- In the language of quantifiers, it means that forall x :: k,
-- there exists a y :: v such that P x y.
--
-- For an instance of Decidable (Found P), it
-- means that for all x :: k, we can prove or disprove the fact
-- that there exists a y :: v such that P x
-- y.
data Found :: ParamPred k v -> Predicate k
-- | A constraint that a ParamPred k v s "selectable". It
-- means that for any input x :: k, we can always find a y
-- :: v that satisfies P x @@ y. We can "select" that
-- y, no matter what.
type Selectable p = Provable (Found p)
-- | The proving/selecting function for Selectable p.
--
-- Must be called by applying the ParamPred:
--
--
-- select @p
--
select :: forall p. Selectable p => Prove (Found p)
-- | A constraint that a ParamPred k v is "searchable". It
-- means that for any input x :: k, we can prove or disprove
-- that there exists a y :: v that satisfies P x @@ y.
-- We can "search" for that y, and prove that it can or cannot
-- be found.
type Searchable p = Decidable (Found p)
-- | The deciding/searching function for Searchable p.
--
-- Must be called by applying the ParamPred:
--
--
-- search @p
--
search :: forall p. Searchable p => Decide (Found p)
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
-- P is satisfied for a specific a at compile-time.
module Data.Type.Predicate.Auto
-- | Automatically generate a witness for predicate p applied to
-- input a.
--
-- Mostly useful for situations where you know a at
-- compile-time, so you can just write auto directly in your
-- source code. The choice is intended to mirror the auto
-- keyword in languages like Idris.
--
-- Very close in nature to the Known typeclass in the
-- type-combinators library.
class Auto (p :: Predicate k) (a :: k)
-- | Have the compiler generate a witness for p @@ a.
--
-- Must be called using type application syntax:
--
--
-- auto _ p @a
--
auto :: Auto p a => p @@ a
-- | Typeclass representing Elems pointing to an a :: k
-- that can be generated automatically from type-level collection as
-- :: f k.
--
-- 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 Auto for the In
-- predicate.
--
-- Example usage:
--
--
-- autoElem :: Index '[1,6,2,3] 2
-- -- IS (IS IZ) -- third spot
--
--
-- And when used with Auto:
--
--
-- auto _ (In [] '[1,6,2,3]) @2
-- -- IS (IS IZ)
--
class AutoElem f (as :: f k) (a :: k)
-- | Generate the Elem pointing to the a :: in a
-- type-level collection as :: f k.
autoElem :: AutoElem f as a => Elem f as a
-- | Helper "predicate transformer" that gives you an instant auto
-- for any Provable instance.
--
-- For example, say you have predicate P that you know is
-- Provable, and you wish to generate a P @@ x, for some
-- specific x you know at compile-time. You can use:
--
--
-- auto _ (AutoProvable P) @x
--
--
-- to obtain a P @@ x.
--
-- AutoProvable is essentially the identity function.
data AutoProvable :: Predicate k -> Predicate k
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.Base.Maybe ('GHC.Base.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 (f :: * -> *) (as :: f k) (a :: k). Data.Type.Predicate.Auto.AutoElem f as a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.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.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
-- | Represent a decidable subset of a type-level collection.
module Data.Type.Universe.Subset
-- | A Subset f p is a predicate that some decidable subset
-- of an input as is true.
data Subset f :: (k ~> Type) -> (f k ~> Type)
-- | A WitSubset f p as describes a
-- decidable subset of type-level collection as.
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 Subset 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
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
-- decidable subset as a result.
mapSubset :: Universe f => (p --> q) -> (q --> p) -> (Subset f p --> Subset f q)
-- | mapSubset, but providing an Elem.
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 Subset into a list (or any Alternative) 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 Subset 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)