{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} -- | -- Module : Data.Type.Predicate -- Copyright : (c) Justin Le 2018 -- License : BSD3 -- -- Maintainer : justin@jle.im -- Stability : experimental -- Portability : non-portable -- -- Combinators for working with type-level predicates, along with -- typeclasses for canonical proofs and deciding functions. -- module Data.Type.Predicate ( -- * Predicates Predicate, Wit(..) -- ** Construct Predicates , TyPred, Evident, EqualTo, BoolPred, Impossible, In -- ** Manipulate predicates , PMap, type Not, decideNot -- * Provable Predicates , Prove, type (-->), type (-->#) , Provable(..) , Disprovable, disprove , ProvableTC, proveTC , TFunctor(..) , compImpl -- * Decidable Predicates , Decide, type (-?>), type (-?>#) , Decidable(..) , DecidableTC, decideTC , DFunctor(..) -- * Manipulate Decisions , Decision(..) , flipDecision, mapDecision , elimDisproof , forgetDisproof, forgetProof, isProved, isDisproved , mapRefuted ) where import Data.Functor.Identity import Data.Kind import Data.List.NonEmpty (NonEmpty(..)) import Data.Maybe import Data.Singletons import Data.Singletons.Decide import Data.Singletons.Prelude hiding (Not, ElemSym1) import Data.Singletons.Prelude.Identity import Data.Type.Functor.Product import Data.Void import qualified Data.Singletons.Prelude.List.NonEmpty as NE -- | 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). In some contexts, this -- is also known as a dependently typed "view". -- -- 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: -- -- 1. 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. -- -- 2. 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 -- | 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 -- @ data Evident :: Predicate k type instance Apply Evident a = Sing a -- | The always-false predicate -- -- Could also be defined as @'ConstSym1' Void@, but this defintion gives -- us a free 'Decidable' instance. -- -- @ -- 'Impossible' :: 'Predicate' k -- @ type Impossible = (Not Evident :: Predicate k) -- | @'EqualTo' a@ is a predicate that the input is equal to @a@. -- -- @ -- 'EqualTo' :: k -> 'Predicate' k -- @ 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) = (PMap p (EqualTo 'True) :: 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) -- | 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 { Wit p a -> p @@ a getWit :: p @@ a } -- | 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 proving function for predicate @p@; in some contexts, also called -- a "view function". 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) infixr 1 -?> infixr 1 -?># infixr 1 --> infixr 1 --># -- | 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: -- -- 1. The decision function for every predicate is available via the -- same name -- -- 2. 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 where -- | 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 -- @ -- -- See 'decideTC' and 'DecidableTC' for a version that isn't ambiguously -- typed, but only works when @p@ is a type constructor. decide :: Decide p default decide :: Provable p => Decide p decide = Apply p a -> Decision (Apply p a) forall a. a -> Decision a Proved (Apply p a -> Decision (Apply p a)) -> (Sing a -> Apply p a) -> Sing a -> Decision (Apply p a) forall b c a. (b -> c) -> (a -> b) -> a -> c . Provable p => Prove p forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p -- | A typeclass for provable predicates (constructivist tautologies). In -- some context, these are also known as "views". -- -- 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". -- -- We can call a type a view if, for any input @a@, there is /some/ -- constructor of @p \@\@ a@ that can we can use to "categorize" @a@. -- -- This typeclass associates a canonical proof function for every provable -- predicate, or a canonical view function for any view. -- -- It confers two main advatnages: -- -- 1. The proof function/view for every predicate/view is available via -- the same name -- -- 2. 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 where -- | The canonical proving function for predicate @p@ (or a canonical -- view function for view @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 -- @ -- -- See 'proveTC' and 'ProvableTC' for a version that isn't ambiguously -- typed, but only works when @p@ is a type constructor. prove :: 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) disprove :: Prove (Not p) disprove = Provable (Not p) => Prove (Not p) forall k1 (p :: k1 ~> *). Provable p => Prove p prove @(Not 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'@). Useful because 'decideTC' doesn't require anything fancy like -- TypeApplications to use. -- -- Also is in this library for compatiblity with "traditional" predicates -- that are GADT type constructors. -- -- @since 0.1.1.0 type DecidableTC p = Decidable (TyPred p) -- | The canonical deciding function for @'DecidableTC' t@. -- -- Note that because @t@ must be an injective type constructor, you can use -- this without explicit type applications; the instance of 'DecidableTC' -- can be inferred from the result type. -- -- @since 0.1.1.0 decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a) decideTC :: Sing a -> Decision (t a) decideTC = Decidable (TyPred t) => Decide (TyPred t) forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @(TyPred t) -- | 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'@). -- Useful because 'proveTC' doesn't require anything fancy like -- TypeApplications to use. -- -- Also is in this library for compatiblity with "traditional" predicates -- that are GADT type constructors. -- -- @since 0.1.1.0 type ProvableTC p = Provable (TyPred p) -- | The canonical proving function for @'DecidableTC' t@. -- -- Note that because @t@ must be an injective type constructor, you can use -- this without explicit type applications; the instance of 'ProvableTC' -- can be inferred from the result type. -- -- @since 0.1.1.0 proveTC :: forall t a. ProvableTC t => Sing a -> t a proveTC :: Sing a -> t a proveTC = Provable (TyPred t) => Prove (TyPred t) forall k1 (p :: k1 ~> *). Provable p => Prove p prove @(TyPred t) -- | Implicatons @p '-?>' q@ can be lifted "through" a 'DFunctor' into an -- @f p '-?>' f q@. class DFunctor f where dmap :: forall p q. (p -?> q) -> (f p -?> f q) -- | Implicatons @p '-->' q@ can be lifted "through" a 'TFunctor' into an -- @f p '-->' f q@. class TFunctor f where tmap :: forall p q. (p --> q) -> (f p --> f q) instance (SDecide k, SingI (a :: k)) => Decidable (EqualTo a) where decide :: Sing a -> Decision (EqualTo a @@ a) decide = (Sing a forall k (a :: k). SingI a => Sing a sing Sing a -> Sing a -> Decision (a :~: a) forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b) %~) instance Decidable Evident instance Provable Evident where prove :: Sing a -> Evident @@ a prove = Sing a -> Evident @@ a forall a. a -> a id -- | @since 3.0.0 instance Decidable (TyPred WrappedSing) -- | @since 3.0.0 instance Provable (TyPred WrappedSing) where prove :: Sing a -> TyPred WrappedSing @@ a prove = Sing a -> TyPred WrappedSing @@ a forall k (a :: k). Sing a -> WrappedSing a WrapSing -- | @since 3.0.0 instance Provable p => Provable (TyPred (Rec (Wit p))) where prove :: Sing a -> TyPred (Rec (Wit p)) @@ a prove = (forall (a :: u). Sing a -> Wit p a) -> Prod [] Sing a -> Prod [] (Wit p) a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd ((p @@ a) -> Wit p a forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Provable p => Prove p forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p) (Rec Sing a -> Rec (Wit p) a) -> (SList a -> Rec Sing a) -> SList a -> Rec (Wit p) a forall b c a. (b -> c) -> (a -> b) -> a -> c . SList a -> Rec Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (Rec (Wit p))) where decide :: Sing a -> Decision (TyPred (Rec (Wit p)) @@ a) decide = \case SNil -> Rec (Wit p) '[] -> Decision (Rec (Wit p) '[]) forall a. a -> Decision a Proved Rec (Wit p) '[] forall u (a :: u -> *). Rec a '[] RNil x `SCons` xs -> case Sing n1 -> Decision (p @@ n1) forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p Sing n1 x of Proved p :: p @@ n1 p -> case Sing n2 -> Decision (Rec (Wit p) n2) forall k1 (t :: k1 -> *) (a :: k1). DecidableTC t => Sing a -> Decision (t a) decideTC Sing n2 xs of Proved ps :: Rec (Wit p) n2 ps -> Rec (Wit p) (n1 : n2) -> Decision (TyPred (Rec (Wit p)) @@ a) forall a. a -> Decision a Proved (Rec (Wit p) (n1 : n2) -> Decision (TyPred (Rec (Wit p)) @@ a)) -> Rec (Wit p) (n1 : n2) -> Decision (TyPred (Rec (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ (p @@ n1) -> Wit p n1 forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit p @@ n1 p Wit p n1 -> Rec (Wit p) n2 -> Rec (Wit p) (n1 : n2) forall u (a :: u -> *) (r :: u) (rs :: [u]). a r -> Rec a rs -> Rec a (r : rs) :& Rec (Wit p) n2 ps Disproved vs :: Refuted (Rec (Wit p) n2) vs -> Refuted (Rec (Wit p) (n1 : n2)) -> Decision (TyPred (Rec (Wit p)) @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (Rec (Wit p) (n1 : n2)) -> Decision (TyPred (Rec (Wit p)) @@ a)) -> Refuted (Rec (Wit p) (n1 : n2)) -> Decision (TyPred (Rec (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ \case _ :& ps :: Rec (Wit p) rs ps -> Refuted (Rec (Wit p) n2) vs Rec (Wit p) n2 Rec (Wit p) rs ps Disproved v :: Refuted (p @@ n1) v -> Refuted (Rec (Wit p) (n1 : n2)) -> Decision (TyPred (Rec (Wit p)) @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (Rec (Wit p) (n1 : n2)) -> Decision (TyPred (Rec (Wit p)) @@ a)) -> Refuted (Rec (Wit p) (n1 : n2)) -> Decision (TyPred (Rec (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ \case Wit p :& _ -> Refuted (p @@ n1) v p @@ n1 p @@ r p -- | @since 3.0.0 instance Provable (TyPred (Rec WrappedSing)) where prove :: Sing a -> TyPred (Rec WrappedSing) @@ a prove = (forall (a :: u). Sing a -> WrappedSing a) -> Prod [] Sing a -> Prod [] WrappedSing a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd forall (a :: u). Sing a -> WrappedSing a forall k (a :: k). Sing a -> WrappedSing a WrapSing (Rec Sing a -> Rec WrappedSing a) -> (SList a -> Rec Sing a) -> SList a -> Rec WrappedSing a forall b c a. (b -> c) -> (a -> b) -> a -> c . SList a -> Rec Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable (TyPred (Rec WrappedSing)) -- | @since 3.0.0 instance Provable p => Provable (TyPred (PMaybe (Wit p))) where prove :: Sing a -> TyPred (PMaybe (Wit p)) @@ a prove = (forall (a :: k). Sing a -> Wit p a) -> Prod Maybe Sing a -> Prod Maybe (Wit p) a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd ((p @@ a) -> Wit p a forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Provable p => Prove p forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p) (PMaybe Sing a -> PMaybe (Wit p) a) -> (SMaybe a -> PMaybe Sing a) -> SMaybe a -> PMaybe (Wit p) a forall b c a. (b -> c) -> (a -> b) -> a -> c . SMaybe a -> PMaybe Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where decide :: Sing a -> Decision (TyPred (PMaybe (Wit p)) @@ a) decide = \case SNothing -> PMaybe (Wit p) 'Nothing -> Decision (PMaybe (Wit p) 'Nothing) forall a. a -> Decision a Proved PMaybe (Wit p) 'Nothing forall k (a :: k -> *). PMaybe a 'Nothing PNothing SJust x -> (Apply p n -> PMaybe (Wit p) ('Just n)) -> (PMaybe (Wit p) ('Just n) -> Apply p n) -> Decision (Apply p n) -> Decision (PMaybe (Wit p) ('Just n)) forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision (Wit p n -> PMaybe (Wit p) ('Just n) forall k (a :: k -> *) (a1 :: k). a a1 -> PMaybe a ('Just a1) PJust (Wit p n -> PMaybe (Wit p) ('Just n)) -> (Apply p n -> Wit p n) -> Apply p n -> PMaybe (Wit p) ('Just n) forall b c a. (b -> c) -> (a -> b) -> a -> c . Apply p n -> Wit p n forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit) (\case PJust (Wit p :: p @@ a1 p) -> Apply p n p @@ a1 p) (Decision (Apply p n) -> Decision (PMaybe (Wit p) ('Just n))) -> (Sing n -> Decision (Apply p n)) -> Sing n -> Decision (PMaybe (Wit p) ('Just n)) forall b c a. (b -> c) -> (a -> b) -> a -> c . Decidable p => Decide p forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p (Sing n -> Decision (TyPred (PMaybe (Wit p)) @@ a)) -> Sing n -> Decision (TyPred (PMaybe (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ Sing n x -- | @since 3.0.0 instance Provable (TyPred (PMaybe WrappedSing)) where prove :: Sing a -> TyPred (PMaybe WrappedSing) @@ a prove = (forall (a :: k). Sing a -> WrappedSing a) -> Prod Maybe Sing a -> Prod Maybe WrappedSing a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd forall (a :: k). Sing a -> WrappedSing a forall k (a :: k). Sing a -> WrappedSing a WrapSing (PMaybe Sing a -> PMaybe WrappedSing a) -> (SMaybe a -> PMaybe Sing a) -> SMaybe a -> PMaybe WrappedSing a forall b c a. (b -> c) -> (a -> b) -> a -> c . SMaybe a -> PMaybe Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable (TyPred (PMaybe WrappedSing)) -- | @since 3.0.0 instance Provable p => Provable (TyPred (NERec (Wit p))) where prove :: Sing a -> TyPred (NERec (Wit p)) @@ a prove = (forall (a :: k). Sing a -> Wit p a) -> Prod NonEmpty Sing a -> Prod NonEmpty (Wit p) a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd ((p @@ a) -> Wit p a forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Provable p => Prove p forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p) (NERec Sing a -> NERec (Wit p) a) -> (SNonEmpty a -> NERec Sing a) -> SNonEmpty a -> NERec (Wit p) a forall b c a. (b -> c) -> (a -> b) -> a -> c . SNonEmpty a -> NERec Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (NERec (Wit p))) where decide :: Sing a -> Decision (TyPred (NERec (Wit p)) @@ a) decide = \case x NE.:%| xs -> case Sing n1 -> Decision (p @@ n1) forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p Sing n1 x of Proved p :: p @@ n1 p -> case Sing n2 -> Decision (Rec (Wit p) n2) forall k1 (t :: k1 -> *) (a :: k1). DecidableTC t => Sing a -> Decision (t a) decideTC Sing n2 xs of Proved ps :: Rec (Wit p) n2 ps -> NERec (Wit p) (n1 ':| n2) -> Decision (TyPred (NERec (Wit p)) @@ a) forall a. a -> Decision a Proved (NERec (Wit p) (n1 ':| n2) -> Decision (TyPred (NERec (Wit p)) @@ a)) -> NERec (Wit p) (n1 ':| n2) -> Decision (TyPred (NERec (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ (p @@ n1) -> Wit p n1 forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit p @@ n1 p Wit p n1 -> Rec (Wit p) n2 -> NERec (Wit p) (n1 ':| n2) forall k (a :: k -> *) (a1 :: k) (as :: [k]). a a1 -> Rec a as -> NERec a (a1 ':| as) :&| Rec (Wit p) n2 ps Disproved vs :: Refuted (Rec (Wit p) n2) vs -> Refuted (NERec (Wit p) (n1 ':| n2)) -> Decision (TyPred (NERec (Wit p)) @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (NERec (Wit p) (n1 ':| n2)) -> Decision (TyPred (NERec (Wit p)) @@ a)) -> Refuted (NERec (Wit p) (n1 ':| n2)) -> Decision (TyPred (NERec (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ \case _ :&| ps :: Rec (Wit p) as ps -> Refuted (Rec (Wit p) n2) vs Rec (Wit p) n2 Rec (Wit p) as ps Disproved v :: Refuted (p @@ n1) v -> Refuted (NERec (Wit p) (n1 ':| n2)) -> Decision (TyPred (NERec (Wit p)) @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (NERec (Wit p) (n1 ':| n2)) -> Decision (TyPred (NERec (Wit p)) @@ a)) -> Refuted (NERec (Wit p) (n1 ':| n2)) -> Decision (TyPred (NERec (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ \case Wit p :&| _ -> Refuted (p @@ n1) v p @@ n1 p @@ a1 p -- | @since 3.0.0 instance Provable (TyPred (NERec WrappedSing)) where prove :: Sing a -> TyPred (NERec WrappedSing) @@ a prove = (forall (a :: k). Sing a -> WrappedSing a) -> Prod NonEmpty Sing a -> Prod NonEmpty WrappedSing a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd forall (a :: k). Sing a -> WrappedSing a forall k (a :: k). Sing a -> WrappedSing a WrapSing (NERec Sing a -> NERec WrappedSing a) -> (SNonEmpty a -> NERec Sing a) -> SNonEmpty a -> NERec WrappedSing a forall b c a. (b -> c) -> (a -> b) -> a -> c . SNonEmpty a -> NERec Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable (TyPred (NERec WrappedSing)) -- | @since 3.0.0 instance Provable p => Provable (TyPred (PIdentity (Wit p))) where prove :: Sing a -> TyPred (PIdentity (Wit p)) @@ a prove = (forall (a :: k). Sing a -> Wit p a) -> Prod Identity Sing a -> Prod Identity (Wit p) a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd ((p @@ a) -> Wit p a forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Provable p => Prove p forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p) (PIdentity Sing a -> PIdentity (Wit p) a) -> (SIdentity a -> PIdentity Sing a) -> SIdentity a -> PIdentity (Wit p) a forall b c a. (b -> c) -> (a -> b) -> a -> c . SIdentity a -> PIdentity Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where decide :: Sing a -> Decision (TyPred (PIdentity (Wit p)) @@ a) decide = \case SIdentity x -> (Apply p n -> PIdentity (Wit p) ('Identity n)) -> (PIdentity (Wit p) ('Identity n) -> Apply p n) -> Decision (Apply p n) -> Decision (PIdentity (Wit p) ('Identity n)) forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision (Wit p n -> PIdentity (Wit p) ('Identity n) forall k (a :: k -> *) (a1 :: k). a a1 -> PIdentity a ('Identity a1) PIdentity (Wit p n -> PIdentity (Wit p) ('Identity n)) -> (Apply p n -> Wit p n) -> Apply p n -> PIdentity (Wit p) ('Identity n) forall b c a. (b -> c) -> (a -> b) -> a -> c . Apply p n -> Wit p n forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit) (\case PIdentity (Wit p :: p @@ a1 p) -> Apply p n p @@ a1 p) (Decision (Apply p n) -> Decision (PIdentity (Wit p) ('Identity n))) -> (Sing n -> Decision (Apply p n)) -> Sing n -> Decision (PIdentity (Wit p) ('Identity n)) forall b c a. (b -> c) -> (a -> b) -> a -> c . Decidable p => Decide p forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p (Sing n -> Decision (TyPred (PIdentity (Wit p)) @@ a)) -> Sing n -> Decision (TyPred (PIdentity (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ Sing n x -- | @since 3.0.0 instance Provable (TyPred (PIdentity WrappedSing)) where prove :: Sing a -> TyPred (PIdentity WrappedSing) @@ a prove = (forall (a :: k). Sing a -> WrappedSing a) -> Prod Identity Sing a -> Prod Identity WrappedSing a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd forall (a :: k). Sing a -> WrappedSing a forall k (a :: k). Sing a -> WrappedSing a WrapSing (PIdentity Sing a -> PIdentity WrappedSing a) -> (SIdentity a -> PIdentity Sing a) -> SIdentity a -> PIdentity WrappedSing a forall b c a. (b -> c) -> (a -> b) -> a -> c . SIdentity a -> PIdentity Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable (TyPred (PIdentity WrappedSing)) -- | @since 3.0.0 instance Provable p => Provable (TyPred (PEither (Wit p))) where prove :: Sing a -> TyPred (PEither (Wit p)) @@ a prove = (forall (a :: k). Sing a -> Wit p a) -> Prod (Either j) Sing a -> Prod (Either j) (Wit p) a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd ((p @@ a) -> Wit p a forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Provable p => Prove p forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p) (PEither Sing a -> PEither (Wit p) a) -> (SEither a -> PEither Sing a) -> SEither a -> PEither (Wit p) a forall b c a. (b -> c) -> (a -> b) -> a -> c . SEither a -> PEither Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (PEither (Wit p))) where decide :: Sing a -> Decision (TyPred (PEither (Wit p)) @@ a) decide = \case SLeft x -> PEither (Wit p) ('Left n) -> Decision (TyPred (PEither (Wit p)) @@ a) forall a. a -> Decision a Proved (PEither (Wit p) ('Left n) -> Decision (TyPred (PEither (Wit p)) @@ a)) -> PEither (Wit p) ('Left n) -> Decision (TyPred (PEither (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ Sing n -> PEither (Wit p) ('Left n) forall j k (e :: j) (a :: k -> *). Sing e -> PEither a ('Left e) PLeft Sing n x SRight y -> (Apply p n -> PEither (Wit p) ('Right n)) -> (PEither (Wit p) ('Right n) -> Apply p n) -> Decision (Apply p n) -> Decision (PEither (Wit p) ('Right n)) forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision (Wit p n -> PEither (Wit p) ('Right n) forall k j (a :: k -> *) (a1 :: k). a a1 -> PEither a ('Right a1) PRight (Wit p n -> PEither (Wit p) ('Right n)) -> (Apply p n -> Wit p n) -> Apply p n -> PEither (Wit p) ('Right n) forall b c a. (b -> c) -> (a -> b) -> a -> c . Apply p n -> Wit p n forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit) (\case PRight (Wit p :: p @@ a1 p) -> Apply p n p @@ a1 p) (Decision (Apply p n) -> Decision (PEither (Wit p) ('Right n))) -> (Sing n -> Decision (Apply p n)) -> Sing n -> Decision (PEither (Wit p) ('Right n)) forall b c a. (b -> c) -> (a -> b) -> a -> c . Decidable p => Decide p forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p (Sing n -> Decision (TyPred (PEither (Wit p)) @@ a)) -> Sing n -> Decision (TyPred (PEither (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ Sing n y -- | @since 3.0.0 instance Provable (TyPred (PEither WrappedSing)) where prove :: Sing a -> TyPred (PEither WrappedSing) @@ a prove = (forall (a :: k). Sing a -> WrappedSing a) -> Prod (Either j) Sing a -> Prod (Either j) WrappedSing a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd forall (a :: k). Sing a -> WrappedSing a forall k (a :: k). Sing a -> WrappedSing a WrapSing (PEither Sing a -> PEither WrappedSing a) -> (SEither a -> PEither Sing a) -> SEither a -> PEither WrappedSing a forall b c a. (b -> c) -> (a -> b) -> a -> c . SEither a -> PEither Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable (TyPred (PEither WrappedSing)) -- | @since 3.0.0 instance Provable p => Provable (TyPred (PTup (Wit p))) where prove :: Sing a -> TyPred (PTup (Wit p)) @@ a prove = (forall (a :: k). Sing a -> Wit p a) -> Prod ((,) j) Sing a -> Prod ((,) j) (Wit p) a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd ((p @@ a) -> Wit p a forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Provable p => Prove p forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p) (PTup Sing a -> PTup (Wit p) a) -> (STuple2 a -> PTup Sing a) -> STuple2 a -> PTup (Wit p) a forall b c a. (b -> c) -> (a -> b) -> a -> c . STuple2 a -> PTup Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable p => Decidable (TyPred (PTup (Wit p))) where decide :: Sing a -> Decision (TyPred (PTup (Wit p)) @@ a) decide (STuple2 x y) = (Apply p n2 -> PTup (Wit p) '(n1, n2)) -> (PTup (Wit p) '(n1, n2) -> Apply p n2) -> Decision (Apply p n2) -> Decision (PTup (Wit p) '(n1, n2)) forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision (Sing n1 -> Wit p n2 -> PTup (Wit p) '(n1, n2) forall j k (w :: j) (a :: k -> *) (a1 :: k). Sing w -> a a1 -> PTup a '(w, a1) PTup Sing n1 x (Wit p n2 -> PTup (Wit p) '(n1, n2)) -> (Apply p n2 -> Wit p n2) -> Apply p n2 -> PTup (Wit p) '(n1, n2) forall b c a. (b -> c) -> (a -> b) -> a -> c . Apply p n2 -> Wit p n2 forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a Wit) (\case PTup _ (Wit p :: p @@ a1 p) -> Apply p n2 p @@ a1 p) (Decision (Apply p n2) -> Decision (PTup (Wit p) '(n1, n2))) -> (Sing n2 -> Decision (Apply p n2)) -> Sing n2 -> Decision (PTup (Wit p) '(n1, n2)) forall b c a. (b -> c) -> (a -> b) -> a -> c . Decidable p => Decide p forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p (Sing n2 -> Decision (TyPred (PTup (Wit p)) @@ a)) -> Sing n2 -> Decision (TyPred (PTup (Wit p)) @@ a) forall a b. (a -> b) -> a -> b $ Sing n2 y -- | @since 3.0.0 instance Provable (TyPred (PTup WrappedSing)) where prove :: Sing a -> TyPred (PTup WrappedSing) @@ a prove = (forall (a :: k). Sing a -> WrappedSing a) -> Prod ((,) j) Sing a -> Prod ((,) j) WrappedSing a forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k). FProd f => (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as mapProd forall (a :: k). Sing a -> WrappedSing a forall k (a :: k). Sing a -> WrappedSing a WrapSing (PTup Sing a -> PTup WrappedSing a) -> (STuple2 a -> PTup Sing a) -> STuple2 a -> PTup WrappedSing a forall b c a. (b -> c) -> (a -> b) -> a -> c . STuple2 a -> PTup Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | @since 3.0.0 instance Decidable (TyPred (PTup WrappedSing)) instance (Decidable p, SingI f) => Decidable (PMap f p) where decide :: Sing a -> Decision (PMap f p @@ a) decide = Decidable p => Decide p forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p (Sing (Apply f a) -> Decision (p @@ Apply f a)) -> (Sing a -> Sing (Apply f a)) -> Sing a -> Decision (p @@ Apply f a) forall b c a. (b -> c) -> (a -> b) -> a -> c . SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t) forall k1 k2 (f :: k1 ~> k2). SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t) applySing (Sing f forall k (a :: k). SingI a => Sing a sing :: Sing f) instance (Provable p, SingI f) => Provable (PMap f p) where prove :: Sing a -> PMap f p @@ a prove = Provable p => Prove p forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p (Sing (Apply f a) -> p @@ Apply f a) -> (Sing a -> Sing (Apply f a)) -> Sing a -> p @@ Apply f a forall b c a. (b -> c) -> (a -> b) -> a -> c . SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t) forall k1 k2 (f :: k1 ~> k2). SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t) applySing (Sing f forall k (a :: k). SingI a => Sing a sing :: Sing f) -- | Compose two implications. compImpl :: forall p q r. () => p --> q -> q --> r -> p --> r compImpl :: (p --> q) -> (q --> r) -> p --> r compImpl f :: p --> q f g :: q --> r g s :: Sing a s = Sing a -> (q @@ a) -> Apply r a q --> r g Sing a s ((q @@ a) -> Apply r a) -> (Apply p a -> q @@ a) -> Apply p a -> Apply r a forall b c a. (b -> c) -> (a -> b) -> a -> c . Sing a -> Apply p a -> q @@ a p --> q f Sing a s -- | @'Not' p@ is the predicate that @p@ is not true. data Not :: Predicate k -> Predicate k type instance Apply (Not p) a = Refuted (p @@ a) instance Decidable p => Decidable (Not p) where decide :: Sing a -> Decision (Not p @@ a) decide (x :: Sing a) = Decision (p @@ a) -> Decision (Not p @@ a) forall k1 (p :: k1 ~> *) (a :: k1). Decision (p @@ a) -> Decision (Not p @@ a) decideNot @p @a (Sing a -> Decision (p @@ a) forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p Sing a x) instance Provable (Not Impossible) where prove :: Sing a -> Not Impossible @@ a prove x :: Sing a x v :: Sing a -> Void v = Void -> Void forall a. Void -> a absurd (Void -> Void) -> Void -> Void forall a b. (a -> b) -> a -> b $ Sing a -> Void v Sing a x -- | Decide @'Not' p@ based on decisions of @p@. decideNot :: forall p a. () => Decision (p @@ a) -> Decision (Not p @@ a) decideNot :: Decision (p @@ a) -> Decision (Not p @@ a) decideNot = Decision (p @@ a) -> Decision (Not p @@ a) forall a. Decision a -> Decision (Refuted a) flipDecision -- | 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 constructivist logic See -- 'Data.Type.Predicate.Logic.doubleNegation' for a situation where it is. -- -- @since 0.1.1.0 flipDecision :: Decision a -> Decision (Refuted a) flipDecision :: Decision a -> Decision (Refuted a) flipDecision = \case Proved p :: a p -> Refuted (Refuted a) -> Decision (Refuted a) forall a. Refuted a -> Decision a Disproved (Refuted a -> Refuted a forall a b. (a -> b) -> a -> b $ a p) Disproved v :: Refuted a v -> Refuted a -> Decision (Refuted a) forall a. a -> Decision a Proved Refuted a v -- | Map over the value inside a 'Decision'. mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision f :: a -> b f g :: b -> a g = \case Proved p :: a p -> b -> Decision b forall a. a -> Decision a Proved (b -> Decision b) -> b -> Decision b forall a b. (a -> b) -> a -> b $ a -> b f a p Disproved v :: Refuted a v -> Refuted b -> Decision b forall a. Refuted a -> Decision a Disproved (Refuted b -> Decision b) -> Refuted b -> Decision b forall a b. (a -> b) -> a -> b $ (b -> a) -> Refuted a -> Refuted b forall a b. (a -> b) -> Refuted b -> Refuted a mapRefuted b -> a g Refuted a v -- | Converts a 'Decision' to a 'Maybe'. Drop the witness of disproof of -- @a@, returning 'Just' if 'Proved' (with the proof) and 'Nothing' if -- 'Disproved'. -- -- @since 0.1.1.0 forgetDisproof :: Decision a -> Maybe a forgetDisproof :: Decision a -> Maybe a forgetDisproof = \case Proved p :: a p -> a -> Maybe a forall a. a -> Maybe a Just a p Disproved _ -> Maybe a forall a. Maybe a Nothing -- | Drop the witness of proof of @a@, returning 'Nothing' if 'Proved' and -- 'Just' if 'Disproved' (with the disproof). -- -- @since 0.1.1.0 forgetProof :: Decision a -> Maybe (Refuted a) forgetProof :: Decision a -> Maybe (Refuted a) forgetProof = Decision (Refuted a) -> Maybe (Refuted a) forall a. Decision a -> Maybe a forgetDisproof (Decision (Refuted a) -> Maybe (Refuted a)) -> (Decision a -> Decision (Refuted a)) -> Decision a -> Maybe (Refuted a) forall b c a. (b -> c) -> (a -> b) -> a -> c . Decision a -> Decision (Refuted a) forall a. Decision a -> Decision (Refuted a) flipDecision -- | Boolean test if a 'Decision' is 'Proved'. -- -- @since 0.1.1.0 isProved :: Decision a -> Bool isProved :: Decision a -> Bool isProved = Maybe a -> Bool forall a. Maybe a -> Bool isJust (Maybe a -> Bool) -> (Decision a -> Maybe a) -> Decision a -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . Decision a -> Maybe a forall a. Decision a -> Maybe a forgetDisproof -- | Boolean test if a 'Decision' is 'Disproved'. -- -- @since 0.1.1.0 isDisproved :: Decision a -> Bool isDisproved :: Decision a -> Bool isDisproved = Maybe a -> Bool forall a. Maybe a -> Bool isNothing (Maybe a -> Bool) -> (Decision a -> Maybe a) -> Decision a -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . Decision a -> Maybe a forall a. Decision a -> Maybe a forgetDisproof -- | Helper function for a common pattern of eliminating the disproved -- branch of 'Decision' to certaintify the proof. -- -- @since 0.1.2.0 elimDisproof :: Decision a -> Refuted (Refuted a) -> a elimDisproof :: Decision a -> Refuted (Refuted a) -> a elimDisproof = \case Proved p :: a p -> a -> Refuted (Refuted a) -> a forall a b. a -> b -> a const a p Disproved v :: Refuted a v -> Void -> a forall a. Void -> a absurd (Void -> a) -> (Refuted (Refuted a) -> Void) -> Refuted (Refuted a) -> a forall b c a. (b -> c) -> (a -> b) -> a -> c . (Refuted (Refuted a) -> Refuted (Refuted a) forall a b. (a -> b) -> a -> b $ Refuted a v) -- | Change the target of a 'Refuted' with a contravariant mapping -- function. -- -- @since 0.1.2.0 mapRefuted :: (a -> b) -> Refuted b -> Refuted a mapRefuted :: (a -> b) -> Refuted b -> Refuted a mapRefuted = (Refuted b -> (a -> b) -> Refuted a) -> (a -> b) -> Refuted b -> Refuted a forall a b c. (a -> b -> c) -> b -> a -> c flip Refuted b -> (a -> b) -> Refuted a forall b c a. (b -> c) -> (a -> b) -> a -> c (.) -- | @'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 instance (SDecide k, SingI (as :: [k])) => Decidable (In [] as) where decide :: forall a. Sing a -> Decision (Index as a) decide :: Sing a -> Decision (Index as a) decide x :: Sing a x = Sing as -> Decision (Index as a) forall (bs :: [k]). Sing bs -> Decision (Index bs a) go (SingI as => Sing as forall k (a :: k). SingI a => Sing a sing @as) where go :: Sing bs -> Decision (Index bs a) go :: Sing bs -> Decision (Index bs a) go = \case SNil -> Refuted (Index bs a) -> Decision (Index bs a) forall a. Refuted a -> Decision a Disproved (Refuted (Index bs a) -> Decision (Index bs a)) -> Refuted (Index bs a) -> Decision (Index bs a) forall a b. (a -> b) -> a -> b $ \case {} y `SCons` ys -> case Sing a x Sing a -> Sing n1 -> Decision (a :~: n1) forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b) %~ Sing n1 y of Proved Refl -> Index (a : n2) a -> Decision (Index (a : n2) a) forall a. a -> Decision a Proved Index (a : n2) a forall k (b :: k) (as :: [k]). Index (b : as) b IZ Disproved v :: Refuted (a :~: n1) v -> case Sing n2 -> Decision (Index n2 a) forall (bs :: [k]). Sing bs -> Decision (Index bs a) go Sing n2 ys of Proved i :: Index n2 a i -> Index (n1 : n2) a -> Decision (Index (n1 : n2) a) forall a. a -> Decision a Proved (Index n2 a -> Index (n1 : n2) a forall k (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 : bs) b IS Index n2 a i) Disproved u :: Refuted (Index n2 a) u -> Refuted (Index bs a) -> Decision (Index bs a) forall a. Refuted a -> Decision a Disproved (Refuted (Index bs a) -> Decision (Index bs a)) -> Refuted (Index bs a) -> Decision (Index bs a) forall a b. (a -> b) -> a -> b $ \case IZ -> Refuted (a :~: n1) v a :~: n1 forall k (a :: k). a :~: a Refl IS i :: Index bs a i -> Refuted (Index n2 a) u Index n2 a Index bs a i instance (SDecide k, SingI (as :: Maybe k)) => Decidable (In Maybe as) where decide :: Sing a -> Decision (In Maybe as @@ a) decide x :: Sing a x = case SingI as => Sing as forall k (a :: k). SingI a => Sing a sing @as of SNothing -> Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a)) -> Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a) forall a b. (a -> b) -> a -> b $ \case {} SJust y -> case Sing a x Sing a -> Sing n -> Decision (a :~: n) forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b) %~ Sing n y of Proved Refl -> IJust ('Just a) a -> Decision (IJust ('Just a) a) forall a. a -> Decision a Proved IJust ('Just a) a forall k (b :: k). IJust ('Just b) b IJust Disproved v :: Refuted (a :~: n) v -> Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a)) -> Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a) forall a b. (a -> b) -> a -> b $ \case IJust -> Refuted (a :~: n) v a :~: n forall k (a :: k). a :~: a Refl instance (SDecide k, SingI (as :: Either j k)) => Decidable (In (Either j) as) where decide :: Sing a -> Decision (In (Either j) as @@ a) decide x :: Sing a x = case SingI as => Sing as forall k (a :: k). SingI a => Sing a sing @as of SLeft _ -> Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a)) -> Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a) forall a b. (a -> b) -> a -> b $ \case {} SRight y -> case Sing a x Sing a -> Sing n -> Decision (a :~: n) forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b) %~ Sing n y of Proved Refl -> IRight ('Right a) a -> Decision (IRight ('Right a) a) forall a. a -> Decision a Proved IRight ('Right a) a forall k j (b :: k). IRight ('Right b) b IRight Disproved v :: Refuted (a :~: n) v -> Refuted (IRight ('Right n) a) -> Decision (In (Either j) as @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (IRight ('Right n) a) -> Decision (In (Either j) as @@ a)) -> Refuted (IRight ('Right n) a) -> Decision (In (Either j) as @@ a) forall a b. (a -> b) -> a -> b $ \case IRight -> Refuted (a :~: n) v a :~: n forall k (a :: k). a :~: a Refl instance (SDecide k, SingI (as :: NonEmpty k)) => Decidable (In NonEmpty as) where decide :: Sing a -> Decision (In NonEmpty as @@ a) decide x :: Sing a x = case SingI as => Sing as forall k (a :: k). SingI a => Sing a sing @as of y NE.:%| (Sing :: Sing bs) -> case Sing a x Sing a -> Sing n1 -> Decision (a :~: n1) forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b) %~ Sing n1 y of Proved Refl -> NEIndex (a ':| n2) a -> Decision (NEIndex (a ':| n2) a) forall a. a -> Decision a Proved NEIndex (a ':| n2) a forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b NEHead Disproved v :: Refuted (a :~: n1) v -> case Sing a -> Decision (In [] n2 @@ a) forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @(In [] bs) Sing a x of Proved i :: In [] n2 @@ a i -> NEIndex (n1 ':| n2) a -> Decision (In NonEmpty as @@ a) forall a. a -> Decision a Proved (NEIndex (n1 ':| n2) a -> Decision (In NonEmpty as @@ a)) -> NEIndex (n1 ':| n2) a -> Decision (In NonEmpty as @@ a) forall a b. (a -> b) -> a -> b $ Index n2 a -> NEIndex (n1 ':| n2) a forall k (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 ':| as) b NETail Index n2 a In [] n2 @@ a i Disproved u :: Refuted (In [] n2 @@ a) u -> Refuted (NEIndex (n1 ':| n2) a) -> Decision (In NonEmpty as @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (NEIndex (n1 ':| n2) a) -> Decision (In NonEmpty as @@ a)) -> Refuted (NEIndex (n1 ':| n2) a) -> Decision (In NonEmpty as @@ a) forall a b. (a -> b) -> a -> b $ \case NEHead -> Refuted (a :~: n1) v a :~: n1 forall k (a :: k). a :~: a Refl NETail i :: Index as a i -> Refuted (In [] n2 @@ a) u Index as a In [] n2 @@ a i instance (SDecide k, SingI (as :: (j, k))) => Decidable (In ((,) j) as) where decide :: Sing a -> Decision (In ((,) j) as @@ a) decide x :: Sing a x = case SingI as => Sing as forall k (a :: k). SingI a => Sing a sing @as of STuple2 _ y -> case Sing a x Sing a -> Sing n2 -> Decision (a :~: n2) forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b) %~ Sing n2 y of Proved Refl -> ISnd '(n1, a) a -> Decision (ISnd '(n1, a) a) forall a. a -> Decision a Proved ISnd '(n1, a) a forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b ISnd Disproved v :: Refuted (a :~: n2) v -> Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a)) -> Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a) forall a b. (a -> b) -> a -> b $ \case ISnd -> Refuted (a :~: n2) v a :~: n2 forall k (a :: k). a :~: a Refl instance (SDecide k, SingI (as :: Identity k)) => Decidable (In Identity as) where decide :: Sing a -> Decision (In Identity as @@ a) decide x :: Sing a x = case SingI as => Sing as forall k (a :: k). SingI a => Sing a sing @as of SIdentity y -> case Sing a x Sing a -> Sing n -> Decision (a :~: n) forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b) %~ Sing n y of Proved Refl -> IIdentity ('Identity a) a -> Decision (IIdentity ('Identity a) a) forall a. a -> Decision a Proved IIdentity ('Identity a) a forall k (b :: k). IIdentity ('Identity b) b IId Disproved v :: Refuted (a :~: n) v -> Refuted (IIdentity ('Identity n) a) -> Decision (In Identity as @@ a) forall a. Refuted a -> Decision a Disproved (Refuted (IIdentity ('Identity n) a) -> Decision (In Identity as @@ a)) -> Refuted (IIdentity ('Identity n) a) -> Decision (In Identity as @@ a) forall a b. (a -> b) -> a -> b $ \case IId -> Refuted (a :~: n) v a :~: n forall k (a :: k). a :~: a Refl