{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} -- | -- Module : Data.Type.Universe -- Copyright : (c) Justin Le 2018 -- License : BSD3 -- -- Maintainer : justin@jle.im -- Stability : experimental -- Portability : non-portable -- -- A type family for "containers", intended for allowing lifting of -- predicates on @k@ to be predicates on containers @f k@. -- module Data.Type.Universe ( -- * Universe Elem, In, Universe(..) , singAll -- ** Instances , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IIdentity(..) -- ** Predicates , All, WitAll(..), NotAll , Any, WitAny(..), None , Null, NotNull -- *** Specialized , IsJust, IsNothing, IsRight, IsLeft -- * Decisions and manipulations , decideAny, decideAll , genAll, igenAll , splitSing , pickElem ) where import Data.Functor.Identity import Data.Kind import Data.List.NonEmpty (NonEmpty(..)) import Data.Singletons import Data.Singletons.Decide import Data.Singletons.Prelude hiding (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Null, Not) import Data.Singletons.Prelude.Identity import Data.Type.Functor.Product import Data.Type.Predicate import Data.Type.Predicate.Logic import GHC.Generics ((:*:)(..)) import Prelude hiding (any, all) import qualified Data.Singletons.Prelude.List.NonEmpty as NE -- | 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 where WitAny :: Elem f as a -> p @@ a -> WitAny f p as -- | 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 :: Predicate k -> Predicate (f k) type instance Apply (Any f p) as = WitAny f p as -- | 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 { WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll :: forall a. Elem f as a -> p @@ a } -- | 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 :: Predicate k -> Predicate (f k) type instance Apply (All f p) as = WitAll f p as instance (Universe f, Decidable p) => Decidable (Any f p) where decide :: Sing a -> Decision (Any f p @@ a) decide = Universe f => Decide p -> Decide (Any f p) forall (f :: * -> *) k (p :: k ~> *). Universe f => Decide p -> Decide (Any f p) decideAny @f @_ @p (Decide p -> Sing a -> Decision (Any f p @@ a)) -> Decide p -> Sing a -> Decision (Any f p @@ a) forall a b. (a -> b) -> a -> b $ Decidable p => Decide p forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p instance (Universe f, Decidable p) => Decidable (All f p) where decide :: Sing a -> Decision (All f p @@ a) decide = Universe f => Decide p -> Decide (All f p) forall (f :: * -> *) k (p :: k ~> *). Universe f => Decide p -> Decide (All f p) decideAll @f @_ @p (Decide p -> Sing a -> Decision (All f p @@ a)) -> Decide p -> Sing a -> Decision (All f p @@ a) forall a b. (a -> b) -> a -> b $ Decidable p => Decide p forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @p instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p) where instance Provable p => Provable (NotNull f ==> Any f p) where prove :: Sing a -> (NotNull f ==> Any f p) @@ a prove _ (WitAny i :: Elem f a a i s :: Evident @@ a s) = Elem f a a -> (p @@ a) -> WitAny f p a forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem f a a i (Sing a -> p @@ a forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p Sing a Evident @@ a s) instance (Universe f, Provable p) => Provable (All f p) where prove :: Sing a -> All f p @@ a prove xs :: Sing a xs = (forall (a :: k). Elem f a a -> p @@ a) -> All f p @@ a forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem f a a -> p @@ a) -> All f p @@ a) -> (forall (a :: k). Elem f a a -> p @@ a) -> All f p @@ a forall a b. (a -> b) -> a -> b $ \i :: Elem f a a i -> Sing a -> p @@ a forall k1 (p :: k1 ~> *). Provable p => Prove p prove @p (Elem f a a -> Sing a -> Sing a forall k (f :: * -> *) (as :: f k) (a :: k). FProd f => Elem f as a -> Sing as -> Sing a indexSing Elem f a a i Sing a xs) instance Universe f => TFunctor (Any f) where tmap :: (p --> q) -> Any f p --> Any f q tmap f :: p --> q f xs :: Sing a xs (WitAny i x) = Elem f a a -> (q @@ a) -> WitAny f q a forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem f a a i (Sing a -> (p @@ a) -> q @@ a p --> q f (Elem f a a -> Sing a -> Sing a forall k (f :: * -> *) (as :: f k) (a :: k). FProd f => Elem f as a -> Sing as -> Sing a indexSing Elem f a a i Sing a xs) p @@ a x) instance Universe f => TFunctor (All f) where tmap :: (p --> q) -> All f p --> All f q tmap f :: p --> q f xs :: Sing a xs a :: All f p @@ a a = (forall (a :: k1). Elem f a a -> q @@ a) -> Apply (All f q) a forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k1). Elem f a a -> q @@ a) -> Apply (All f q) a) -> (forall (a :: k1). Elem f a a -> q @@ a) -> Apply (All f q) a forall a b. (a -> b) -> a -> b $ \i :: Elem f a a i -> Sing a -> (p @@ a) -> q @@ a p --> q f (Elem f a a -> Sing a -> Sing a forall k (f :: * -> *) (as :: f k) (a :: k). FProd f => Elem f as a -> Sing as -> Sing a indexSing Elem f a a i Sing a xs) (WitAll f p a -> Elem f a a -> p @@ a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All f p @@ a WitAll f p a a Elem f a a i) instance Universe f => DFunctor (All f) where dmap :: (p -?> q) -> All f p -?> All f q dmap f :: p -?> q f xs :: Sing a xs a :: All f p @@ a a = (forall (a :: k1). Elem f a a -> Sing a -> Decision (q @@ a)) -> Sing a -> Decision (Apply (All f q) a) forall (f :: * -> *) k (p :: k ~> *) (as :: f k). Universe f => (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All f p @@ as) idecideAll (\i :: Elem f a a i x :: Sing a x -> Sing a -> (p @@ a) -> Decision (q @@ a) p -?> q f Sing a x (WitAll f p a -> Elem f a a -> p @@ a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All f p @@ a WitAll f p a a Elem f a a i)) Sing a xs -- | Typeclass for a type-level container that you can quantify or lift -- type-level predicates over. class FProd f => Universe (f :: Type -> Type) where -- | 'decideAny', but providing an 'Elem'. idecideAny :: forall k (p :: k ~> Type) (as :: f k). () => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -- ^ predicate on value -> (Sing as -> Decision (Any f p @@ as)) -- ^ predicate on collection -- | 'decideAll', but providing an 'Elem'. idecideAll :: forall k (p :: k ~> Type) (as :: f k). () => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -- ^ predicate on value -> (Sing as -> Decision (All f p @@ as)) -- ^ predicate on collection allProd :: forall p g. () => (forall a. Sing a -> p @@ a -> g a) -> All f p --> TyPred (Prod f g) prodAll :: forall p g as. () => (forall a. g a -> p @@ a) -> Prod f g as -> All f p @@ as -- | 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)) -- | 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)) -- | A @'NotAll' f p@ is a predicate on a collection @as@ that at least one -- @a@ in @as@ does not satisfy predicate @p@. type NotAll f p = (Not (All 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 -- ^ predicate on value -> Decide (Any f p) -- ^ predicate on collection decideAny :: Decide p -> Decide (Any f p) decideAny f :: Decide p f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a)) -> Sing a -> Decision (Apply (Any f p) a) forall (f :: * -> *) k (p :: k ~> *) (as :: f k). Universe f => (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any f p @@ as) idecideAny ((Sing a -> Decision (Apply p a)) -> Elem f a a -> Sing a -> Decision (Apply p a) forall a b. a -> b -> a const Sing a -> Decision (Apply p a) Decide p f) -- | 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 -- ^ predicate on value -> Decide (All f p) -- ^ predicate on collection decideAll :: Decide p -> Decide (All f p) decideAll f :: Decide p f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a)) -> Sing a -> Decision (Apply (All f p) a) forall (f :: * -> *) k (p :: k ~> *) (as :: f k). Universe f => (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All f p @@ as) idecideAll ((Sing a -> Decision (Apply p a)) -> Elem f a a -> Sing a -> Decision (Apply p a) forall a b. a -> b -> a const Sing a -> Decision (Apply p a) Decide p f) -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist. splitSing :: forall f k (as :: f k). Universe f => Sing as -> All f (TyPred Sing) @@ as splitSing :: Sing as -> All f (TyPred Sing) @@ as splitSing = (forall (a :: k). Sing a -> TyPred Sing @@ a) -> Prod f Sing as -> All f (TyPred Sing) @@ as forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *) (as :: f k). Universe f => (forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as prodAll forall (a :: k). Sing a -> TyPred Sing @@ a forall a. a -> a id (Prod f Sing as -> WitAll f (TyPred Sing) as) -> (Sing as -> Prod f Sing as) -> Sing as -> WitAll f (TyPred Sing) as forall b c a. (b -> c) -> (a -> b) -> a -> c . Sing as -> Prod f Sing as forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | 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) pickElem :: Decision (Elem f as a) pickElem = (WitAny f (TyCon ((:~:) a)) as -> Elem f as a) -> (Elem f as a -> WitAny f (TyCon ((:~:) a)) as) -> Decision (WitAny f (TyCon ((:~:) a)) as) -> Decision (Elem f as a) forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision (\case WitAny i :: Elem f as a i Refl -> Elem f as a Elem f as a i) (\case i :: Elem f as a i -> Elem f as a -> (TyCon ((:~:) a) @@ a) -> WitAny f (TyCon ((:~:) a)) as forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem f as a i TyCon ((:~:) a) @@ a forall k (a :: k). a :~: a Refl) (Decision (WitAny f (TyCon ((:~:) a)) as) -> Decision (Elem f as a)) -> (Sing as -> Decision (WitAny f (TyCon ((:~:) a)) as)) -> Sing as -> Decision (Elem f as a) forall b c a. (b -> c) -> (a -> b) -> a -> c . Decidable (Any f (TyCon ((:~:) a))) => Decide (Any f (TyCon ((:~:) a))) forall k1 (p :: k1 ~> *). Decidable p => Decide p decide @(Any f (TyPred ((:~:) a))) (Sing as -> Decision (Elem f as a)) -> Sing as -> Decision (Elem f as a) forall a b. (a -> b) -> a -> b $ Sing as forall k (a :: k). SingI a => Sing a sing -- | '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) -- ^ always-true predicate on value -> (Sing as -> All f p @@ as) -- ^ always-true predicate on collection igenAll :: (forall (a :: k). Elem f as a -> Sing a -> p @@ a) -> Sing as -> All f p @@ as igenAll f :: forall (a :: k). Elem f as a -> Sing a -> p @@ a f = (forall (a :: k). (:*:) (Elem f as) Sing a -> p @@ a) -> Prod f (Elem f as :*: Sing) as -> All f p @@ as forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *) (as :: f k). Universe f => (forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as prodAll (\(i :*: x) -> Elem f as a -> Sing a -> p @@ a forall (a :: k). Elem f as a -> Sing a -> p @@ a f Elem f as a i Sing a x) (Prod f (Elem f as :*: Sing) as -> WitAll f p as) -> (Sing as -> Prod f (Elem f as :*: Sing) as) -> Sing as -> WitAll f p as forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (a :: k). Elem f as a -> Sing a -> (:*:) (Elem f as) Sing a) -> Prod f Sing as -> Prod f (Elem f as :*: Sing) as forall k (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *). FProd f => (forall (a :: k). Elem f as a -> g a -> h a) -> Prod f g as -> Prod f h as imapProd forall (a :: k). Elem f as a -> Sing a -> (:*:) (Elem f as) Sing a forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> g p -> (:*:) f g p (:*:) (Prod f Sing as -> Prod f (Elem f as :*: Sing) as) -> (Sing as -> Prod f Sing as) -> Sing as -> Prod f (Elem f as :*: Sing) as forall b c a. (b -> c) -> (a -> b) -> a -> c . Sing as -> Prod f Sing as forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | 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 -- ^ always-true predicate on value -> Prove (All f p) -- ^ always-true predicate on collection genAll :: Prove p -> Prove (All f p) genAll f :: Prove p f = Prove p -> Prod f Sing a -> Apply (All f p) a forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *) (as :: f k). Universe f => (forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as prodAll Prove p f (Prod f Sing a -> WitAll f p a) -> (Sing a -> Prod f Sing a) -> Sing a -> WitAll f p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Sing a -> Prod f Sing a forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist. singAll :: forall f k (as :: f k). Universe f => Sing as -> All f Evident @@ as singAll :: Sing as -> All f Evident @@ as singAll = (forall (a :: k). Sing a -> Evident @@ a) -> Prod f Sing as -> All f Evident @@ as forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *) (as :: f k). Universe f => (forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as prodAll forall (a :: k). Sing a -> Evident @@ a forall a. a -> a id (Prod f Sing as -> WitAll f Evident as) -> (Sing as -> Prod f Sing as) -> Sing as -> WitAll f Evident as forall b c a. (b -> c) -> (a -> b) -> a -> c . Sing as -> Prod f Sing as forall (f :: * -> *) k (as :: f k). FProd f => Sing as -> Prod f Sing as singProd -- | Test that a 'Maybe' is 'Just'. -- -- @since 0.1.2.0 type IsJust = (NotNull Maybe :: Predicate (Maybe k)) -- | Test that a 'Maybe' is 'Nothing'. -- -- @since 0.1.2.0 type IsNothing = (Null Maybe :: Predicate (Maybe k)) -- | Test that an 'Either' is 'Right' -- -- @since 0.1.2.0 type IsRight = (NotNull (Either j) :: Predicate (Either j k)) -- | Test that an 'Either' is 'Left' -- -- @since 0.1.2.0 type IsLeft = (Null (Either j) :: Predicate (Either j k)) instance Universe [] where idecideAny :: forall k (p :: k ~> Type) (as :: [k]). () => (forall a. Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any [] p @@ as) idecideAny :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any [] p @@ as) idecideAny f :: forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a) f = \case SNil -> Refuted (WitAny [] p '[]) -> Decision (Any [] p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAny [] p '[]) -> Decision (Any [] p @@ as)) -> Refuted (WitAny [] p '[]) -> Decision (Any [] p @@ as) forall a b. (a -> b) -> a -> b $ \case WitAny i :: Elem [] '[] a i _ -> case Elem [] '[] a i of {} x `SCons` xs -> case Elem [] as n1 -> Sing n1 -> Decision (p @@ n1) forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a) f Elem [] as n1 forall k (b :: k) (as :: [k]). Index (b : as) b IZ Sing n1 x of Proved p :: p @@ n1 p -> WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as) forall a. a -> Decision a Proved (WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as)) -> WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as) forall a b. (a -> b) -> a -> b $ Elem [] (n1 : n2) n1 -> (p @@ n1) -> WitAny [] p (n1 : n2) forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem [] (n1 : n2) n1 forall k (b :: k) (as :: [k]). Index (b : as) b IZ p @@ n1 p Disproved v :: Refuted (p @@ n1) v -> case (forall (a :: k). Elem [] n2 a -> Sing a -> Decision (p @@ a)) -> Sing n2 -> Decision (Any [] p @@ n2) forall (f :: * -> *) k (p :: k ~> *) (as :: f k). Universe f => (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any f p @@ as) idecideAny @[] @_ @p (Index (n1 : n2) a -> Sing a -> Decision (Apply p a) forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a) f (Index (n1 : n2) a -> Sing a -> Decision (Apply p a)) -> (Index n2 a -> Index (n1 : n2) a) -> Index n2 a -> Sing a -> Decision (Apply p a) forall b c a. (b -> c) -> (a -> b) -> a -> c . Index n2 a -> Index (n1 : n2) a forall k (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 : bs) b IS) Sing n2 xs of Proved (WitAny i p) -> WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as) forall a. a -> Decision a Proved (WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as)) -> WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as) forall a b. (a -> b) -> a -> b $ Elem [] (n1 : n2) a -> (p @@ a) -> WitAny [] p (n1 : n2) forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny (Index n2 a -> Index (n1 : n2) a forall k (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 : bs) b IS Elem [] n2 a Index n2 a i) p @@ a p Disproved vs :: Refuted (Any [] p @@ n2) vs -> Refuted (WitAny [] p (n1 : n2)) -> Decision (Any [] p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAny [] p (n1 : n2)) -> Decision (Any [] p @@ as)) -> Refuted (WitAny [] p (n1 : n2)) -> Decision (Any [] p @@ as) forall a b. (a -> b) -> a -> b $ \case WitAny IZ p :: p @@ a p -> Refuted (p @@ n1) v p @@ n1 p @@ a p WitAny (IS i) p :: p @@ a p -> Refuted (Any [] p @@ n2) vs (Elem [] n2 a -> (p @@ a) -> WitAny [] p n2 forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem [] n2 a Index bs a i p @@ a p) idecideAll :: forall k (p :: k ~> Type) (as :: [k]). () => (forall a. Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All [] p @@ as) idecideAll :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All [] p @@ as) idecideAll f :: forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a) f = \case SNil -> WitAll [] p '[] -> Decision (All [] p @@ as) forall a. a -> Decision a Proved (WitAll [] p '[] -> Decision (All [] p @@ as)) -> WitAll [] p '[] -> Decision (All [] p @@ as) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[] forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]) -> (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[] forall a b. (a -> b) -> a -> b $ \case {} x `SCons` xs -> case Elem [] as n1 -> Sing n1 -> Decision (p @@ n1) forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a) f Elem [] as n1 forall k (b :: k) (as :: [k]). Index (b : as) b IZ Sing n1 x of Proved p :: p @@ n1 p -> case (forall (a :: k). Elem [] n2 a -> Sing a -> Decision (p @@ a)) -> Sing n2 -> Decision (All [] p @@ n2) forall (f :: * -> *) k (p :: k ~> *) (as :: f k). Universe f => (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All f p @@ as) idecideAll @[] @_ @p (Index (n1 : n2) a -> Sing a -> Decision (Apply p a) forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a) f (Index (n1 : n2) a -> Sing a -> Decision (Apply p a)) -> (Index n2 a -> Index (n1 : n2) a) -> Index n2 a -> Sing a -> Decision (Apply p a) forall b c a. (b -> c) -> (a -> b) -> a -> c . Index n2 a -> Index (n1 : n2) a forall k (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 : bs) b IS) Sing n2 xs of Proved a :: All [] p @@ n2 a -> WitAll [] p (n1 : n2) -> Decision (All [] p @@ as) forall a. a -> Decision a Proved (WitAll [] p (n1 : n2) -> Decision (All [] p @@ as)) -> WitAll [] p (n1 : n2) -> Decision (All [] p @@ as) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem [] (n1 : n2) a -> p @@ a) -> WitAll [] p (n1 : n2) forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem [] (n1 : n2) a -> p @@ a) -> WitAll [] p (n1 : n2)) -> (forall (a :: k). Elem [] (n1 : n2) a -> p @@ a) -> WitAll [] p (n1 : n2) forall a b. (a -> b) -> a -> b $ \case IZ -> p @@ n1 Apply p a p IS i -> WitAll [] p n2 -> Elem [] n2 a -> Apply p a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All [] p @@ n2 WitAll [] p n2 a Elem [] n2 a Index bs a i Disproved v :: Refuted (All [] p @@ n2) v -> Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as)) -> Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as) forall a b. (a -> b) -> a -> b $ \a :: WitAll [] p (n1 : n2) a -> Refuted (All [] p @@ n2) v Refuted (All [] p @@ n2) -> Refuted (All [] p @@ n2) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2 forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll (WitAll [] p (n1 : n2) -> forall (a :: k). Elem [] (n1 : n2) a -> p @@ a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll [] p (n1 : n2) a (Index (n1 : n2) a -> Apply p a) -> (Index n2 a -> Index (n1 : n2) a) -> Index n2 a -> Apply p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Index n2 a -> Index (n1 : n2) a forall k (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 : bs) b IS) Disproved v :: Refuted (p @@ n1) v -> Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as)) -> Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as) forall a b. (a -> b) -> a -> b $ \a :: WitAll [] p (n1 : n2) a -> Refuted (p @@ n1) v Refuted (p @@ n1) -> Refuted (p @@ n1) forall a b. (a -> b) -> a -> b $ WitAll [] p (n1 : n2) -> Elem [] (n1 : n2) n1 -> p @@ n1 forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll [] p (n1 : n2) a Elem [] (n1 : n2) n1 forall k (b :: k) (as :: [k]). Index (b : as) b IZ allProd :: forall p g. () => (forall a. Sing a -> p @@ a -> g a) -> All [] p --> TyPred (Prod [] g) allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All [] p --> TyPred (Prod [] g) allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a f = Sing a -> Apply (All [] p) a -> Apply (TyPred (Prod [] g)) a forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as go where go :: Sing as -> WitAll [] p as -> Prod [] g as go :: Sing as -> WitAll [] p as -> Prod [] g as go = \case SNil -> \_ -> Prod [] g as forall u (a :: u -> *). Rec a '[] RNil x `SCons` xs -> \a :: WitAll [] p as a -> Sing n1 -> (p @@ n1) -> g n1 forall (a :: k). Sing a -> (p @@ a) -> g a f Sing n1 x (WitAll [] p as -> Elem [] as n1 -> p @@ n1 forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll [] p as a Elem [] as n1 forall k (b :: k) (as :: [k]). Index (b : as) b IZ) g n1 -> Rec g n2 -> Rec g (n1 : n2) forall u (a :: u -> *) (r :: u) (rs :: [u]). a r -> Rec a rs -> Rec a (r : rs) :& Sing n2 -> WitAll [] p n2 -> Prod [] g n2 forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as go Sing n2 xs ((forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2 forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll (WitAll [] p as -> forall (a :: k). Elem [] as a -> p @@ a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll [] p as a (Index (n1 : n2) a -> Apply p a) -> (Index n2 a -> Index (n1 : n2) a) -> Index n2 a -> Apply p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Index n2 a -> Index (n1 : n2) a forall k (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 : bs) b IS)) prodAll :: forall p g as. () => (forall a. g a -> p @@ a) -> Prod [] g as -> All [] p @@ as prodAll :: (forall (a :: k). g a -> p @@ a) -> Prod [] g as -> All [] p @@ as prodAll f :: forall (a :: k). g a -> p @@ a f = Prod [] g as -> All [] p @@ as forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs go where go :: Prod [] g bs -> All [] p @@ bs go :: Prod [] g bs -> All [] p @@ bs go = \case RNil -> (forall (a :: k). Elem [] '[] a -> p @@ a) -> All [] p @@ bs forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem [] '[] a -> p @@ a) -> All [] p @@ bs) -> (forall (a :: k). Elem [] '[] a -> p @@ a) -> All [] p @@ bs forall a b. (a -> b) -> a -> b $ \case {} x :& xs -> (forall (a :: k). Elem [] (r : rs) a -> p @@ a) -> All [] p @@ bs forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem [] (r : rs) a -> p @@ a) -> All [] p @@ bs) -> (forall (a :: k). Elem [] (r : rs) a -> p @@ a) -> All [] p @@ bs forall a b. (a -> b) -> a -> b $ \case IZ -> g r -> p @@ r forall (a :: k). g a -> p @@ a f g r x IS i -> WitAll [] p rs -> Elem [] rs a -> Apply p a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll (Prod [] g rs -> All [] p @@ rs forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs go Prod [] g rs Rec g rs xs) Elem [] rs a Index bs a i instance Universe Maybe where idecideAny :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any Maybe p @@ as) idecideAny f :: forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a) f = \case SNothing -> Refuted (WitAny Maybe p 'Nothing) -> Decision (Any Maybe p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAny Maybe p 'Nothing) -> Decision (Any Maybe p @@ as)) -> Refuted (WitAny Maybe p 'Nothing) -> Decision (Any Maybe p @@ as) forall a b. (a -> b) -> a -> b $ \case WitAny i :: Elem Maybe 'Nothing a i _ -> case Elem Maybe 'Nothing a i of {} SJust x -> case Elem Maybe as n -> Sing n -> Decision (p @@ n) forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a) f Elem Maybe as n forall k (b :: k). IJust ('Just b) b IJust Sing n x of Proved p :: p @@ n p -> WitAny Maybe p ('Just n) -> Decision (Any Maybe p @@ as) forall a. a -> Decision a Proved (WitAny Maybe p ('Just n) -> Decision (Any Maybe p @@ as)) -> WitAny Maybe p ('Just n) -> Decision (Any Maybe p @@ as) forall a b. (a -> b) -> a -> b $ Elem Maybe ('Just n) n -> (p @@ n) -> WitAny Maybe p ('Just n) forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem Maybe ('Just n) n forall k (b :: k). IJust ('Just b) b IJust p @@ n p Disproved v :: Refuted (p @@ n) v -> Refuted (WitAny Maybe p ('Just n)) -> Decision (Any Maybe p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAny Maybe p ('Just n)) -> Decision (Any Maybe p @@ as)) -> Refuted (WitAny Maybe p ('Just n)) -> Decision (Any Maybe p @@ as) forall a b. (a -> b) -> a -> b $ \case WitAny IJust p :: p @@ a p -> Refuted (p @@ n) v p @@ n p @@ a p idecideAll :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All Maybe p @@ as) idecideAll f :: forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a) f = \case SNothing -> WitAll Maybe p 'Nothing -> Decision (All Maybe p @@ as) forall a. a -> Decision a Proved (WitAll Maybe p 'Nothing -> Decision (All Maybe p @@ as)) -> WitAll Maybe p 'Nothing -> Decision (All Maybe p @@ as) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a) -> WitAll Maybe p 'Nothing forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem Maybe 'Nothing a -> p @@ a) -> WitAll Maybe p 'Nothing) -> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a) -> WitAll Maybe p 'Nothing forall a b. (a -> b) -> a -> b $ \case {} SJust x -> case Elem Maybe as n -> Sing n -> Decision (p @@ n) forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a) f Elem Maybe as n forall k (b :: k). IJust ('Just b) b IJust Sing n x of Proved p :: p @@ n p -> WitAll Maybe p ('Just n) -> Decision (All Maybe p @@ as) forall a. a -> Decision a Proved (WitAll Maybe p ('Just n) -> Decision (All Maybe p @@ as)) -> WitAll Maybe p ('Just n) -> Decision (All Maybe p @@ as) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem Maybe ('Just n) a -> p @@ a) -> WitAll Maybe p ('Just n) forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem Maybe ('Just n) a -> p @@ a) -> WitAll Maybe p ('Just n)) -> (forall (a :: k). Elem Maybe ('Just n) a -> p @@ a) -> WitAll Maybe p ('Just n) forall a b. (a -> b) -> a -> b $ \case IJust -> p @@ n Apply p a p Disproved v :: Refuted (p @@ n) v -> Refuted (WitAll Maybe p ('Just n)) -> Decision (All Maybe p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAll Maybe p ('Just n)) -> Decision (All Maybe p @@ as)) -> Refuted (WitAll Maybe p ('Just n)) -> Decision (All Maybe p @@ as) forall a b. (a -> b) -> a -> b $ \a :: WitAll Maybe p ('Just n) a -> Refuted (p @@ n) v Refuted (p @@ n) -> Refuted (p @@ n) forall a b. (a -> b) -> a -> b $ WitAll Maybe p ('Just n) -> Elem Maybe ('Just n) n -> p @@ n forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll Maybe p ('Just n) a Elem Maybe ('Just n) n forall k (b :: k). IJust ('Just b) b IJust allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All Maybe p --> TyPred (Prod Maybe g) allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a f = \case SNothing -> \_ -> Apply (TyPred (Prod Maybe g)) a forall k (a :: k -> *). PMaybe a 'Nothing PNothing SJust x -> \a :: All Maybe p @@ a a -> g n -> PMaybe g ('Just n) forall k (a :: k -> *) (a1 :: k). a a1 -> PMaybe a ('Just a1) PJust (Sing n -> (p @@ n) -> g n forall (a :: k). Sing a -> (p @@ a) -> g a f Sing n x (WitAll Maybe p ('Just n) -> Elem Maybe ('Just n) n -> p @@ n forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All Maybe p @@ a WitAll Maybe p ('Just n) a Elem Maybe ('Just n) n forall k (b :: k). IJust ('Just b) b IJust)) prodAll :: (forall (a :: k). g a -> p @@ a) -> Prod Maybe g as -> All Maybe p @@ as prodAll f :: forall (a :: k). g a -> p @@ a f = \case PNothing -> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a) -> All Maybe p @@ as forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem Maybe 'Nothing a -> p @@ a) -> All Maybe p @@ as) -> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a) -> All Maybe p @@ as forall a b. (a -> b) -> a -> b $ \case {} PJust x -> (forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a) -> All Maybe p @@ as forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a) -> All Maybe p @@ as) -> (forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a) -> All Maybe p @@ as forall a b. (a -> b) -> a -> b $ \case IJust -> g a1 -> p @@ a1 forall (a :: k). g a -> p @@ a f g a1 x instance Universe (Either j) where idecideAny :: (forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (Either j) p @@ as) idecideAny f :: forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a) f = \case SLeft _ -> Refuted (WitAny (Either j) p ('Left n)) -> Decision (Any (Either j) p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAny (Either j) p ('Left n)) -> Decision (Any (Either j) p @@ as)) -> Refuted (WitAny (Either j) p ('Left n)) -> Decision (Any (Either j) p @@ as) forall a b. (a -> b) -> a -> b $ \case WitAny i :: Elem (Either j) ('Left n) a i _ -> case Elem (Either j) ('Left n) a i of {} SRight x -> case Elem (Either j) as n -> Sing n -> Decision (p @@ n) forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a) f Elem (Either j) as n forall k j (b :: k). IRight ('Right b) b IRight Sing n x of Proved p :: p @@ n p -> WitAny (Either j) p ('Right n) -> Decision (Any (Either j) p @@ as) forall a. a -> Decision a Proved (WitAny (Either j) p ('Right n) -> Decision (Any (Either j) p @@ as)) -> WitAny (Either j) p ('Right n) -> Decision (Any (Either j) p @@ as) forall a b. (a -> b) -> a -> b $ Elem (Either j) ('Right n) n -> (p @@ n) -> WitAny (Either j) p ('Right n) forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem (Either j) ('Right n) n forall k j (b :: k). IRight ('Right b) b IRight p @@ n p Disproved v :: Refuted (p @@ n) v -> Refuted (WitAny (Either j) p ('Right n)) -> Decision (Any (Either j) p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAny (Either j) p ('Right n)) -> Decision (Any (Either j) p @@ as)) -> Refuted (WitAny (Either j) p ('Right n)) -> Decision (Any (Either j) p @@ as) forall a b. (a -> b) -> a -> b $ \case WitAny IRight p :: p @@ a p -> Refuted (p @@ n) v p @@ n p @@ a p idecideAll :: (forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (Either j) p @@ as) idecideAll f :: forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a) f = \case SLeft _ -> WitAll (Either j) p ('Left n) -> Decision (All (Either j) p @@ as) forall a. a -> Decision a Proved (WitAll (Either j) p ('Left n) -> Decision (All (Either j) p @@ as)) -> WitAll (Either j) p ('Left n) -> Decision (All (Either j) p @@ as) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a) -> WitAll (Either j) p ('Left n) forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a) -> WitAll (Either j) p ('Left n)) -> (forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a) -> WitAll (Either j) p ('Left n) forall a b. (a -> b) -> a -> b $ \case {} SRight x -> case Elem (Either j) as n -> Sing n -> Decision (p @@ n) forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a) f Elem (Either j) as n forall k j (b :: k). IRight ('Right b) b IRight Sing n x of Proved p :: p @@ n p -> WitAll (Either j) p ('Right n) -> Decision (All (Either j) p @@ as) forall a. a -> Decision a Proved (WitAll (Either j) p ('Right n) -> Decision (All (Either j) p @@ as)) -> WitAll (Either j) p ('Right n) -> Decision (All (Either j) p @@ as) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a) -> WitAll (Either j) p ('Right n) forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a) -> WitAll (Either j) p ('Right n)) -> (forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a) -> WitAll (Either j) p ('Right n) forall a b. (a -> b) -> a -> b $ \case IRight -> p @@ n Apply p a p Disproved v :: Refuted (p @@ n) v -> Refuted (WitAll (Either j) p ('Right n)) -> Decision (All (Either j) p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAll (Either j) p ('Right n)) -> Decision (All (Either j) p @@ as)) -> Refuted (WitAll (Either j) p ('Right n)) -> Decision (All (Either j) p @@ as) forall a b. (a -> b) -> a -> b $ \a :: WitAll (Either j) p ('Right n) a -> Refuted (p @@ n) v Refuted (p @@ n) -> Refuted (p @@ n) forall a b. (a -> b) -> a -> b $ WitAll (Either j) p ('Right n) -> Elem (Either j) ('Right n) n -> p @@ n forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll (Either j) p ('Right n) a Elem (Either j) ('Right n) n forall k j (b :: k). IRight ('Right b) b IRight allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All (Either j) p --> TyPred (Prod (Either j) g) allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a f = \case SLeft w -> \_ -> Sing n -> PEither g ('Left n) forall j k (e :: j) (a :: k -> *). Sing e -> PEither a ('Left e) PLeft Sing n w SRight x -> \a :: All (Either j) p @@ a a -> g n -> PEither g ('Right n) forall k j (a :: k -> *) (a1 :: k). a a1 -> PEither a ('Right a1) PRight (Sing n -> (p @@ n) -> g n forall (a :: k). Sing a -> (p @@ a) -> g a f Sing n x (WitAll (Either j) p ('Right n) -> Elem (Either j) ('Right n) n -> p @@ n forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All (Either j) p @@ a WitAll (Either j) p ('Right n) a Elem (Either j) ('Right n) n forall k j (b :: k). IRight ('Right b) b IRight)) prodAll :: (forall (a :: k). g a -> p @@ a) -> Prod (Either j) g as -> All (Either j) p @@ as prodAll f :: forall (a :: k). g a -> p @@ a f = \case PLeft _ -> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a) -> All (Either j) p @@ as forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a) -> All (Either j) p @@ as) -> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a) -> All (Either j) p @@ as forall a b. (a -> b) -> a -> b $ \case {} PRight x -> (forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a) -> All (Either j) p @@ as forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a) -> All (Either j) p @@ as) -> (forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a) -> All (Either j) p @@ as forall a b. (a -> b) -> a -> b $ \case IRight -> g a1 -> p @@ a1 forall (a :: k). g a -> p @@ a f g a1 x instance Universe NonEmpty where idecideAny :: forall k (p :: k ~> Type) (as :: NonEmpty k). () => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any NonEmpty p @@ as) idecideAny :: (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any NonEmpty p @@ as) idecideAny f :: forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a) f (x NE.:%| xs) = case Elem NonEmpty as n1 -> Sing n1 -> Decision (p @@ n1) forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a) f Elem NonEmpty as n1 forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b NEHead Sing n1 x of Proved p :: p @@ n1 p -> WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as) forall a. a -> Decision a Proved (WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as)) -> WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as) forall a b. (a -> b) -> a -> b $ Elem NonEmpty (n1 ':| n2) n1 -> (p @@ n1) -> WitAny NonEmpty p (n1 ':| n2) forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem NonEmpty (n1 ':| n2) n1 forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b NEHead p @@ n1 p Disproved v :: Refuted (p @@ n1) v -> case (forall (a :: k). Elem [] n2 a -> Sing a -> Decision (p @@ a)) -> Sing n2 -> Decision (Any [] p @@ n2) forall (f :: * -> *) k (p :: k ~> *) (as :: f k). Universe f => (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any f p @@ as) idecideAny @[] @_ @p (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a) forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a) f (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a)) -> (Index n2 a -> NEIndex (n1 ':| n2) a) -> Index n2 a -> Sing a -> Decision (Apply p a) forall b c a. (b -> c) -> (a -> b) -> a -> c . Index n2 a -> NEIndex (n1 ':| n2) a forall k (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 ':| as) b NETail) Sing n2 xs of Proved (WitAny i p) -> WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as) forall a. a -> Decision a Proved (WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as)) -> WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as) forall a b. (a -> b) -> a -> b $ Elem NonEmpty (n1 ':| n2) a -> (p @@ a) -> WitAny NonEmpty p (n1 ':| n2) forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny (Index n2 a -> NEIndex (n1 ':| n2) a forall k (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 ':| as) b NETail Elem [] n2 a Index n2 a i) p @@ a p Disproved vs :: Refuted (Any [] p @@ n2) vs -> Refuted (WitAny NonEmpty p (n1 ':| n2)) -> Decision (Any NonEmpty p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAny NonEmpty p (n1 ':| n2)) -> Decision (Any NonEmpty p @@ as)) -> Refuted (WitAny NonEmpty p (n1 ':| n2)) -> Decision (Any NonEmpty p @@ as) forall a b. (a -> b) -> a -> b $ \case WitAny i :: Elem NonEmpty (n1 ':| n2) a i p :: p @@ a p -> case Elem NonEmpty (n1 ':| n2) a i of NEHead -> Refuted (p @@ n1) v p @@ n1 p @@ a p NETail i' -> Refuted (Any [] p @@ n2) vs (Elem [] n2 a -> (p @@ a) -> WitAny [] p n2 forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem [] n2 a Index as a i' p @@ a p) idecideAll :: forall k (p :: k ~> Type) (as :: NonEmpty k). () => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All NonEmpty p @@ as) idecideAll :: (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All NonEmpty p @@ as) idecideAll f :: forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a) f (x NE.:%| xs) = case Elem NonEmpty as n1 -> Sing n1 -> Decision (p @@ n1) forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a) f Elem NonEmpty as n1 forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b NEHead Sing n1 x of Proved p :: p @@ n1 p -> case (forall (a :: k). Elem [] n2 a -> Sing a -> Decision (p @@ a)) -> Sing n2 -> Decision (All [] p @@ n2) forall (f :: * -> *) k (p :: k ~> *) (as :: f k). Universe f => (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All f p @@ as) idecideAll @[] @_ @p (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a) forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a) f (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a)) -> (Index n2 a -> NEIndex (n1 ':| n2) a) -> Index n2 a -> Sing a -> Decision (Apply p a) forall b c a. (b -> c) -> (a -> b) -> a -> c . Index n2 a -> NEIndex (n1 ':| n2) a forall k (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 ':| as) b NETail) Sing n2 xs of Proved ps :: All [] p @@ n2 ps -> WitAll NonEmpty p (n1 ':| n2) -> Decision (All NonEmpty p @@ as) forall a. a -> Decision a Proved (WitAll NonEmpty p (n1 ':| n2) -> Decision (All NonEmpty p @@ as)) -> WitAll NonEmpty p (n1 ':| n2) -> Decision (All NonEmpty p @@ as) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a) -> WitAll NonEmpty p (n1 ':| n2) forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a) -> WitAll NonEmpty p (n1 ':| n2)) -> (forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a) -> WitAll NonEmpty p (n1 ':| n2) forall a b. (a -> b) -> a -> b $ \case NEHead -> p @@ n1 Apply p a p NETail i -> WitAll [] p n2 -> Elem [] n2 a -> Apply p a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All [] p @@ n2 WitAll [] p n2 ps Elem [] n2 a Index as a i Disproved v :: Refuted (All [] p @@ n2) v -> Refuted (WitAll NonEmpty p (n1 ':| n2)) -> Decision (All NonEmpty p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAll NonEmpty p (n1 ':| n2)) -> Decision (All NonEmpty p @@ as)) -> Refuted (WitAll NonEmpty p (n1 ':| n2)) -> Decision (All NonEmpty p @@ as) forall a b. (a -> b) -> a -> b $ \a :: WitAll NonEmpty p (n1 ':| n2) a -> Refuted (All [] p @@ n2) v Refuted (All [] p @@ n2) -> Refuted (All [] p @@ n2) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2 forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll (WitAll NonEmpty p (n1 ':| n2) -> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll NonEmpty p (n1 ':| n2) a (NEIndex (n1 ':| n2) a -> Apply p a) -> (Index n2 a -> NEIndex (n1 ':| n2) a) -> Index n2 a -> Apply p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Index n2 a -> NEIndex (n1 ':| n2) a forall k (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 ':| as) b NETail) Disproved v :: Refuted (p @@ n1) v -> Refuted (WitAll NonEmpty p (n1 ':| n2)) -> Decision (All NonEmpty p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAll NonEmpty p (n1 ':| n2)) -> Decision (All NonEmpty p @@ as)) -> Refuted (WitAll NonEmpty p (n1 ':| n2)) -> Decision (All NonEmpty p @@ as) forall a b. (a -> b) -> a -> b $ \a :: WitAll NonEmpty p (n1 ':| n2) a -> Refuted (p @@ n1) v Refuted (p @@ n1) -> Refuted (p @@ n1) forall a b. (a -> b) -> a -> b $ WitAll NonEmpty p (n1 ':| n2) -> Elem NonEmpty (n1 ':| n2) n1 -> p @@ n1 forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll NonEmpty p (n1 ':| n2) a Elem NonEmpty (n1 ':| n2) n1 forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b NEHead allProd :: forall p g. () => (forall a. Sing a -> p @@ a -> g a) -> All NonEmpty p --> TyPred (Prod NonEmpty g) allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All NonEmpty p --> TyPred (Prod NonEmpty g) allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a f (x NE.:%| xs) a :: All NonEmpty p @@ a a = Sing n1 -> (p @@ n1) -> g n1 forall (a :: k). Sing a -> (p @@ a) -> g a f Sing n1 x (WitAll NonEmpty p (n1 ':| n2) -> Elem NonEmpty (n1 ':| n2) n1 -> p @@ n1 forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All NonEmpty p @@ a WitAll NonEmpty p (n1 ':| n2) a Elem NonEmpty (n1 ':| n2) n1 forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b NEHead) g n1 -> Rec g n2 -> NERec g (n1 ':| n2) forall k (a :: k -> *) (a1 :: k) (as :: [k]). a a1 -> Rec a as -> NERec a (a1 ':| as) :&| (forall (a :: k). Sing a -> (p @@ a) -> g a) -> Sing n2 -> (All [] p @@ n2) -> TyPred (Prod [] g) @@ n2 forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *). Universe f => (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All f p --> TyPred (Prod f g) allProd @[] @p forall (a :: k). Sing a -> (p @@ a) -> g a f Sing n2 xs ((forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2 forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll (WitAll NonEmpty p (n1 ':| n2) -> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All NonEmpty p @@ a WitAll NonEmpty p (n1 ':| n2) a (NEIndex (n1 ':| n2) a -> Apply p a) -> (Index n2 a -> NEIndex (n1 ':| n2) a) -> Index n2 a -> Apply p a forall b c a. (b -> c) -> (a -> b) -> a -> c . Index n2 a -> NEIndex (n1 ':| n2) a forall k (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 ':| as) b NETail)) prodAll :: forall p g as. () => (forall a. g a -> p @@ a) -> Prod NonEmpty g as -> All NonEmpty p @@ as prodAll :: (forall (a :: k). g a -> p @@ a) -> Prod NonEmpty g as -> All NonEmpty p @@ as prodAll f :: forall (a :: k). g a -> p @@ a f (x :&| xs) = (forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a) -> All NonEmpty p @@ as forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a) -> All NonEmpty p @@ as) -> (forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a) -> All NonEmpty p @@ as forall a b. (a -> b) -> a -> b $ \case NEHead -> g a1 -> p @@ a1 forall (a :: k). g a -> p @@ a f g a1 x NETail i -> WitAll [] p as -> Elem [] as a -> Apply p a forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll ((forall (a :: k). g a -> p @@ a) -> Prod [] g as -> All [] p @@ as forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *) (as :: f k). Universe f => (forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as prodAll @[] @p forall (a :: k). g a -> p @@ a f Prod [] g as Rec g as xs) Elem [] as a Index as a i instance Universe ((,) j) where idecideAny :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any ((,) j) p @@ as) idecideAny f :: forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a) f (STuple2 _ x) = case Elem ((,) j) as n2 -> Sing n2 -> Decision (p @@ n2) forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a) f Elem ((,) j) as n2 forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b ISnd Sing n2 x of Proved p :: p @@ n2 p -> WitAny ((,) j) p '(n1, n2) -> Decision (Any ((,) j) p @@ as) forall a. a -> Decision a Proved (WitAny ((,) j) p '(n1, n2) -> Decision (Any ((,) j) p @@ as)) -> WitAny ((,) j) p '(n1, n2) -> Decision (Any ((,) j) p @@ as) forall a b. (a -> b) -> a -> b $ Elem ((,) j) '(n1, n2) n2 -> (p @@ n2) -> WitAny ((,) j) p '(n1, n2) forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem ((,) j) '(n1, n2) n2 forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b ISnd p @@ n2 p Disproved v :: Refuted (p @@ n2) v -> Refuted (WitAny ((,) j) p '(n1, n2)) -> Decision (Any ((,) j) p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAny ((,) j) p '(n1, n2)) -> Decision (Any ((,) j) p @@ as)) -> Refuted (WitAny ((,) j) p '(n1, n2)) -> Decision (Any ((,) j) p @@ as) forall a b. (a -> b) -> a -> b $ \case WitAny ISnd p :: p @@ a p -> Refuted (p @@ n2) v p @@ n2 p @@ a p idecideAll :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All ((,) j) p @@ as) idecideAll f :: forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a) f (STuple2 _ x) = case Elem ((,) j) as n2 -> Sing n2 -> Decision (p @@ n2) forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a) f Elem ((,) j) as n2 forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b ISnd Sing n2 x of Proved p :: p @@ n2 p -> WitAll ((,) j) p '(n1, n2) -> Decision (All ((,) j) p @@ as) forall a. a -> Decision a Proved (WitAll ((,) j) p '(n1, n2) -> Decision (All ((,) j) p @@ as)) -> WitAll ((,) j) p '(n1, n2) -> Decision (All ((,) j) p @@ as) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a) -> WitAll ((,) j) p '(n1, n2) forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a) -> WitAll ((,) j) p '(n1, n2)) -> (forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a) -> WitAll ((,) j) p '(n1, n2) forall a b. (a -> b) -> a -> b $ \case ISnd -> p @@ n2 Apply p a p Disproved v :: Refuted (p @@ n2) v -> Refuted (WitAll ((,) j) p '(n1, n2)) -> Decision (All ((,) j) p @@ as) forall a. Refuted a -> Decision a Disproved (Refuted (WitAll ((,) j) p '(n1, n2)) -> Decision (All ((,) j) p @@ as)) -> Refuted (WitAll ((,) j) p '(n1, n2)) -> Decision (All ((,) j) p @@ as) forall a b. (a -> b) -> a -> b $ \a :: WitAll ((,) j) p '(n1, n2) a -> Refuted (p @@ n2) v Refuted (p @@ n2) -> Refuted (p @@ n2) forall a b. (a -> b) -> a -> b $ WitAll ((,) j) p '(n1, n2) -> Elem ((,) j) '(n1, n2) n2 -> p @@ n2 forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll WitAll ((,) j) p '(n1, n2) a Elem ((,) j) '(n1, n2) n2 forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b ISnd allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All ((,) j) p --> TyPred (Prod ((,) j) g) allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a f (STuple2 w x) a :: All ((,) j) p @@ a a = Sing n1 -> g n2 -> PTup g '(n1, n2) forall j k (w :: j) (a :: k -> *) (a1 :: k). Sing w -> a a1 -> PTup a '(w, a1) PTup Sing n1 w (g n2 -> Apply (TyPred (Prod ((,) j) g)) a) -> g n2 -> Apply (TyPred (Prod ((,) j) g)) a forall a b. (a -> b) -> a -> b $ Sing n2 -> (p @@ n2) -> g n2 forall (a :: k). Sing a -> (p @@ a) -> g a f Sing n2 x (WitAll ((,) j) p '(n1, n2) -> Elem ((,) j) '(n1, n2) n2 -> p @@ n2 forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All ((,) j) p @@ a WitAll ((,) j) p '(n1, n2) a Elem ((,) j) '(n1, n2) n2 forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b ISnd) prodAll :: (forall (a :: k). g a -> p @@ a) -> Prod ((,) j) g as -> All ((,) j) p @@ as prodAll f :: forall (a :: k). g a -> p @@ a f (PTup _ x) = (forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a) -> All ((,) j) p @@ as forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a) -> All ((,) j) p @@ as) -> (forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a) -> All ((,) j) p @@ as forall a b. (a -> b) -> a -> b $ \case ISnd -> g a1 -> p @@ a1 forall (a :: k). g a -> p @@ a f g a1 x -- | The single-pointed universe. instance Universe Identity where idecideAny :: (forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any Identity p @@ as) idecideAny f :: forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a) f (SIdentity x) = (Apply p n -> WitAny Identity p ('Identity n)) -> (WitAny Identity p ('Identity n) -> Apply p n) -> Decision (Apply p n) -> Decision (WitAny Identity p ('Identity n)) forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision (Elem Identity ('Identity n) n -> Apply p n -> WitAny Identity p ('Identity n) forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *). Elem f as a -> (p @@ a) -> WitAny f p as WitAny Elem Identity ('Identity n) n forall k (b :: k). IIdentity ('Identity b) b IId) (\case WitAny IId p :: p @@ a p -> Apply p n p @@ a p) (Decision (Apply p n) -> Decision (Any Identity p @@ as)) -> Decision (Apply p n) -> Decision (Any Identity p @@ as) forall a b. (a -> b) -> a -> b $ Elem Identity as n -> Sing n -> Decision (Apply p n) forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a) f Elem Identity as n forall k (b :: k). IIdentity ('Identity b) b IId Sing n x idecideAll :: (forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All Identity p @@ as) idecideAll f :: forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a) f (SIdentity x) = (Apply p n -> WitAll Identity p ('Identity n)) -> (WitAll Identity p ('Identity n) -> Apply p n) -> Decision (Apply p n) -> Decision (WitAll Identity p ('Identity n)) forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b mapDecision (\p :: Apply p n p -> (forall (a :: k). Elem Identity ('Identity n) a -> p @@ a) -> WitAll Identity p ('Identity n) forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem Identity ('Identity n) a -> p @@ a) -> WitAll Identity p ('Identity n)) -> (forall (a :: k). Elem Identity ('Identity n) a -> p @@ a) -> WitAll Identity p ('Identity n) forall a b. (a -> b) -> a -> b $ \case IId -> Apply p n Apply p a p) (WitAll Identity p ('Identity n) -> Elem Identity ('Identity n) n -> Apply p n forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a `runWitAll` Elem Identity ('Identity n) n forall k (b :: k). IIdentity ('Identity b) b IId) (Decision (Apply p n) -> Decision (All Identity p @@ as)) -> Decision (Apply p n) -> Decision (All Identity p @@ as) forall a b. (a -> b) -> a -> b $ Elem Identity as n -> Sing n -> Decision (Apply p n) forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a) f Elem Identity as n forall k (b :: k). IIdentity ('Identity b) b IId Sing n x allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All Identity p --> TyPred (Prod Identity g) allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a f (SIdentity x) a :: All Identity p @@ a a = g n -> Apply (TyPred (Prod Identity g)) a forall k (a :: k -> *) (a1 :: k). a a1 -> PIdentity a ('Identity a1) PIdentity (g n -> Apply (TyPred (Prod Identity g)) a) -> g n -> Apply (TyPred (Prod Identity g)) a forall a b. (a -> b) -> a -> b $ Sing n -> (p @@ n) -> g n forall (a :: k). Sing a -> (p @@ a) -> g a f Sing n x (WitAll Identity p ('Identity n) -> Elem Identity ('Identity n) n -> p @@ n forall k (p :: k ~> *) (f :: * -> *) (as :: f k). WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a runWitAll All Identity p @@ a WitAll Identity p ('Identity n) a Elem Identity ('Identity n) n forall k (b :: k). IIdentity ('Identity b) b IId) prodAll :: (forall (a :: k). g a -> p @@ a) -> Prod Identity g as -> All Identity p @@ as prodAll f :: forall (a :: k). g a -> p @@ a f (PIdentity x) = (forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a) -> All Identity p @@ as forall k (f :: * -> *) (p :: k ~> *) (as :: f k). (forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as WitAll ((forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a) -> All Identity p @@ as) -> (forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a) -> All Identity p @@ as forall a b. (a -> b) -> a -> b $ \case IId -> g a1 -> p @@ a1 forall (a :: k). g a -> p @@ a f g a1 x