{-# 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