{-# 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.Either.Singletons hiding    (IsLeft, IsRight)
import           Data.Functor.Identity
import           Data.Functor.Identity.Singletons
import           Data.Kind
import           Data.List.NonEmpty               (NonEmpty(..))
import           Data.List.Singletons hiding      (Elem, ElemSym0, ElemSym1, ElemSym2, All, Any, Null)
import           Data.Maybe.Singletons hiding     (IsJust, IsNothing)
import           Data.Singletons
import           Data.Singletons.Decide
import           Data.Tuple.Singletons
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.List.NonEmpty.Singletons    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 { forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
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 :: Decide (Any f p)
decide = forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (Any f p)
decideAny @f @_ @p forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p

instance (Universe f, Decidable p) => Decidable (All f p) where
    decide :: Decide (All f p)
decide = forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (All f p)
decideAll @f @_ @p forall a b. (a -> b) -> a -> b
$ 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 :: Prove (NotNull f ==> Any f p)
prove Sing a
_ (WitAny Elem f a a
i Evident @@ a
s) = forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i (forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p Evident @@ a
s)

instance (Universe f, Provable p) => Provable (All f p) where
    prove :: Prove (All f p)
prove Sing a
xs = forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \Elem f a a
i -> forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p (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 :: forall (p :: k1 ~> *) (q :: k1 ~> *).
(p --> q) -> Any f p --> Any f q
tmap p --> q
f Sing a
xs (WitAny Elem f a a
i p @@ a
x) = forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i (p --> q
f (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 :: forall (p :: k1 ~> *) (q :: k1 ~> *).
(p --> q) -> All f p --> All f q
tmap p --> q
f Sing a
xs All f p @@ a
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 b. (a -> b) -> a -> b
$ \Elem f a a
i -> p --> q
f (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) (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ a
a Elem f a a
i)

instance Universe f => DFunctor (All f) where
    dmap :: forall (p :: k1 ~> *) (q :: k1 ~> *).
(p -?> q) -> All f p -?> All f q
dmap p -?> q
f Sing a
xs All f p @@ a
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 (\Elem f a a
i Sing a
x -> p -?> q
f Sing a
x (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All 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 :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (Any f p)
decideAny Decide p
f = 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 (forall a b. a -> b -> a
const 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 :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (All f p)
decideAll Decide p
f = 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 (forall a b. a -> b -> a
const 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 :: forall (f :: * -> *) k (as :: f k).
Universe f =>
Sing as -> All f (TyPred Sing) @@ as
splitSing = 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. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (f :: * -> *) k (as :: f k) (a :: k).
(Universe f, SingI as, SingI a, SDecide k) =>
Decision (Elem f as a)
pickElem = forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (\case WitAny Elem f as a
i a :~: a
TyPred ((:~:) a) @@ a
Refl -> Elem f as a
i)
                       (\case Elem f as a
i -> forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f as a
i forall {k} (a :: k). a :~: a
Refl)
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @(Any f (TyPred ((:~:) a)))
         forall a b. (a -> b) -> a -> b
$ 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 (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> p @@ a)
-> Sing as -> All f p @@ as
igenAll forall (a :: k). Elem f as a -> Sing a -> p @@ a
f = 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 (\(Elem f as a
i :*: Sing a
x) -> forall (a :: k). Elem f as a -> Sing a -> p @@ a
f Elem f as a
i Sing a
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Prove p -> Prove (All f p)
genAll Prove p
f = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (f :: * -> *) k (as :: f k).
Universe f =>
Sing as -> All f Evident @@ as
singAll = 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. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 k (p :: k ~> *) (as :: [k]).
(forall (a :: k). 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)
f = \case
      Sing as
SList as
SNil -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
        WitAny Elem [] '[] a
i p @@ a
_ -> case Elem [] '[] a
i of {}
      Sing n1
x `SCons` Sing n2
xs -> case forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ Sing n1
x of
        Proved p @@ n1
p    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ p @@ n1
p
        Disproved Refuted (p @@ n1)
v -> case 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 (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS) Sing n2
xs of
          Proved (WitAny Elem [] n2 a
i p @@ a
p) -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny (forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Elem [] n2 a
i) p @@ a
p
          Disproved Refuted (Any [] p @@ n2)
vs -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
            WitAny Elem [] (n1 : n2) a
Index (n1 : n2) a
IZ     p @@ a
p -> Refuted (p @@ n1)
v p @@ a
p
            WitAny (IS Index bs a
i) p @@ a
p -> Refuted (Any [] p @@ n2)
vs (forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny 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 k (p :: k ~> *) (as :: [k]).
(forall (a :: k). 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)
f = \case
      Sing as
SList as
SNil -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case {}
      Sing n1
x `SCons` Sing n2
xs -> case forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ Sing n1
x of
        Proved p @@ n1
p -> case 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 (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS) Sing n2
xs of
          Proved All [] p @@ n2
a -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case
            Elem [] (n1 : n2) a
Index (n1 : n2) a
IZ   -> p @@ n1
p
            IS Index bs a
i -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ n2
a Index bs a
i
          Disproved Refuted (All [] p @@ n2)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \All [] p @@ as
a -> Refuted (All [] p @@ n2)
v forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ as
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS)
        Disproved Refuted (p @@ n1)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \All [] p @@ as
a -> Refuted (p @@ n1)
v forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ as
a 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 {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All [] p --> TyPred (Prod [] g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f = forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go
      where
        go :: Sing as -> WitAll [] p as -> Prod [] g as
        go :: forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go = \case
          Sing as
SList as
SNil         -> \WitAll [] p as
_ -> forall {u} (a :: u -> *). Rec a '[]
RNil
          Sing n1
x `SCons` Sing n2
xs -> \WitAll [] p as
a -> forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n1
x (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll [] p as
a forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ)
                             forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go Sing n2
xs (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll [] p as
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 {k} (p :: Predicate k) (g :: k -> *) (as :: [k]).
(forall (a :: k). g a -> p @@ a) -> Prod [] g as -> All [] p @@ as
prodAll forall (a :: k). g a -> p @@ a
f = forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go
      where
        go :: Prod [] g bs -> All [] p @@ bs
        go :: forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go = \case
          Prod [] g bs
Rec g bs
RNil    -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case {}
          g r
x :& Rec g rs
xs -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case
            Elem [] (r : rs) a
Index (r : rs) a
IZ   -> forall (a :: k). g a -> p @@ a
f g r
x
            IS Index bs a
i -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go Rec g rs
xs) Index bs a
i

instance Universe Maybe where
    idecideAny :: forall k (p :: k ~> *) (as :: Maybe k).
(forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any Maybe p @@ as)
idecideAny forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f = \case
      Sing as
SMaybe as
SNothing -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case WitAny Elem Maybe 'Nothing a
i p @@ a
_ -> case Elem Maybe 'Nothing a
i of {}
      SJust Sing n
x  -> case forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f forall {k} (b :: k). IJust ('Just b) b
IJust Sing n
x of
        Proved p @@ n
p    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny forall {k} (b :: k). IJust ('Just b) b
IJust p @@ n
p
        Disproved Refuted (p @@ n)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
          WitAny Elem Maybe ('Just n) a
IJust ('Just n) a
IJust p @@ a
p -> Refuted (p @@ n)
v p @@ a
p
    idecideAll :: forall k (p :: k ~> *) (as :: Maybe k).
(forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All Maybe p @@ as)
idecideAll forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f = \case
      Sing as
SMaybe as
SNothing -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case {}
      SJust Sing n
x  -> case forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f forall {k} (b :: k). IJust ('Just b) b
IJust Sing n
x of
        Proved p @@ n
p    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem Maybe ('Just n) a
IJust ('Just n) a
IJust -> p @@ n
p
        Disproved Refuted (p @@ n)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \All Maybe p @@ as
a -> Refuted (p @@ n)
v forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Maybe p @@ as
a forall {k} (b :: k). IJust ('Just b) b
IJust
    allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All Maybe p --> TyPred (Prod Maybe g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f = \case
      Sing a
SMaybe a
SNothing -> \All Maybe p @@ a
_ -> forall {k} (a :: k -> *). PMaybe a 'Nothing
PNothing
      SJust Sing n
x  -> \All Maybe p @@ a
a -> forall {k} (a :: k -> *) (a1 :: k). a a1 -> PMaybe a ('Just a1)
PJust (forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Maybe p @@ a
a forall {k} (b :: k). IJust ('Just b) b
IJust))
    prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: Maybe k).
(forall (a :: k). g a -> p @@ a)
-> Prod Maybe g as -> All Maybe p @@ as
prodAll forall (a :: k). g a -> p @@ a
f = \case
      Prod Maybe g as
PMaybe g as
PNothing -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case {}
      PJust g a1
x  -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem Maybe ('Just a1) a
IJust ('Just a1) a
IJust -> forall (a :: k). g a -> p @@ a
f g a1
x

instance Universe (Either j) where
    idecideAny :: forall k (p :: k ~> *) (as :: Either j k).
(forall (a :: k).
 Elem (Either j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any (Either j) p @@ as)
idecideAny forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f = \case
      SLeft  Sing n
_ -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case WitAny Elem (Either j) ('Left n) a
i p @@ a
_ -> case Elem (Either j) ('Left n) a
i of {}
      SRight Sing n
x -> case forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f forall {k} {j} (b :: k). IRight ('Right b) b
IRight Sing n
x of
        Proved p @@ n
p    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny forall {k} {j} (b :: k). IRight ('Right b) b
IRight p @@ n
p
        Disproved Refuted (p @@ n)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
          WitAny Elem (Either j) ('Right n) a
IRight ('Right n) a
IRight p @@ a
p -> Refuted (p @@ n)
v p @@ a
p
    idecideAll :: forall k (p :: k ~> *) (as :: Either j k).
(forall (a :: k).
 Elem (Either j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All (Either j) p @@ as)
idecideAll forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f = \case
      SLeft  Sing n
_ -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case {}
      SRight Sing n
x -> case forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f forall {k} {j} (b :: k). IRight ('Right b) b
IRight Sing n
x of
        Proved p @@ n
p    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem (Either j) ('Right n) a
IRight ('Right n) a
IRight -> p @@ n
p
        Disproved Refuted (p @@ n)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \All (Either j) p @@ as
a -> Refuted (p @@ n)
v forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All (Either j) p @@ as
a forall {k} {j} (b :: k). IRight ('Right b) b
IRight
    allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All (Either j) p --> TyPred (Prod (Either j) g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f = \case
      SLeft  Sing n
w -> \All (Either j) p @@ a
_ -> forall {j} {k} (e :: j) (a :: k -> *).
Sing e -> PEither a ('Left e)
PLeft Sing n
w
      SRight Sing n
x -> \All (Either j) p @@ a
a -> forall {k} {j} (a :: k -> *) (a1 :: k).
a a1 -> PEither a ('Right a1)
PRight (forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All (Either j) p @@ a
a forall {k} {j} (b :: k). IRight ('Right b) b
IRight))
    prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: Either j k).
(forall (a :: k). g a -> p @@ a)
-> Prod (Either j) g as -> All (Either j) p @@ as
prodAll forall (a :: k). g a -> p @@ a
f = \case
      PLeft Sing e
_  -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case {}
      PRight g a1
x -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem (Either j) ('Right a1) a
IRight ('Right a1) a
IRight -> 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 k (p :: k ~> *) (as :: NonEmpty k).
(forall (a :: k).
 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)
f (Sing n1
x NE.:%| Sing n2
xs) = case forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead Sing n1
x of
      Proved p @@ n1
p    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead p @@ n1
p
      Disproved Refuted (p @@ n1)
v -> case 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 (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail) Sing n2
xs of
        Proved (WitAny Elem [] n2 a
i p @@ a
p) -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny (forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail Elem [] n2 a
i) p @@ a
p
        Disproved Refuted (Any [] p @@ n2)
vs     -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
          WitAny Elem NonEmpty (n1 ':| n2) a
i p @@ a
p -> case Elem NonEmpty (n1 ':| n2) a
i of
            Elem NonEmpty (n1 ':| n2) a
NEIndex (n1 ':| n2) a
NEHead    -> Refuted (p @@ n1)
v p @@ a
p
            NETail Index as a
i' -> Refuted (Any [] p @@ n2)
vs (forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny 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 k (p :: k ~> *) (as :: NonEmpty k).
(forall (a :: k).
 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)
f (Sing n1
x NE.:%| Sing n2
xs) = case forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead Sing n1
x of
      Proved p @@ n1
p -> case 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 (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail) Sing n2
xs of
        Proved All [] p @@ n2
ps -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case
          Elem NonEmpty (n1 ':| n2) a
NEIndex (n1 ':| n2) a
NEHead   -> p @@ n1
p
          NETail Index as a
i -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ n2
ps Index as a
i
        Disproved Refuted (All [] p @@ n2)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \All NonEmpty p @@ as
a -> Refuted (All [] p @@ n2)
v forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ as
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail)
      Disproved Refuted (p @@ n1)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \All NonEmpty p @@ as
a -> Refuted (p @@ n1)
v forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ as
a 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 {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All NonEmpty p --> TyPred (Prod NonEmpty g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f (Sing n1
x NE.:%| Sing n2
xs) All NonEmpty p @@ a
a =
          forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n1
x (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ a
a forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead)
      forall {k} (a :: k -> *) (a1 :: k) (as :: [k]).
a a1 -> Rec a as -> NERec a (a1 ':| as)
:&| 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 k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ a
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 {k} (p :: Predicate k) (g :: k -> *) (as :: NonEmpty k).
(forall (a :: k). g a -> p @@ a)
-> Prod NonEmpty g as -> All NonEmpty p @@ as
prodAll forall (a :: k). g a -> p @@ a
f (g a1
x :&| Rec g as
xs) = forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case
        Elem NonEmpty (a1 ':| as) a
NEIndex (a1 ':| as) a
NEHead   -> forall (a :: k). g a -> p @@ a
f g a1
x
        NETail Index as a
i -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (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 Rec g as
xs) Index as a
i

instance Universe ((,) j) where
    idecideAny :: forall k (p :: k ~> *) (as :: (j, k)).
(forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any ((,) j) p @@ as)
idecideAny forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f (STuple2 Sing n1
_ Sing n2
x) = case forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing n2
x of
      Proved p @@ n2
p    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd p @@ n2
p
      Disproved Refuted (p @@ n2)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case WitAny Elem ((,) j) '(n1, n2) a
ISnd '(n1, n2) a
ISnd p @@ a
p -> Refuted (p @@ n2)
v p @@ a
p
    idecideAll :: forall k (p :: k ~> *) (as :: (j, k)).
(forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All ((,) j) p @@ as)
idecideAll forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f (STuple2 Sing n1
_ Sing n2
x) = case forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing n2
x of
      Proved p @@ n2
p    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem ((,) j) '(n1, n2) a
ISnd '(n1, n2) a
ISnd -> p @@ n2
p
      Disproved Refuted (p @@ n2)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \All ((,) j) p @@ as
a -> Refuted (p @@ n2)
v forall a b. (a -> b) -> a -> b
$ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All ((,) j) p @@ as
a forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd
    allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All ((,) j) p --> TyPred (Prod ((,) j) g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f (STuple2 Sing n1
w Sing n2
x) All ((,) j) p @@ a
a = forall {j} {k} (w :: j) (a :: k -> *) (a1 :: k).
Sing w -> a a1 -> PTup a '(w, a1)
PTup Sing n1
w forall a b. (a -> b) -> a -> b
$ forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n2
x (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All ((,) j) p @@ a
a forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd)
    prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: (j, k)).
(forall (a :: k). g a -> p @@ a)
-> Prod ((,) j) g as -> All ((,) j) p @@ as
prodAll forall (a :: k). g a -> p @@ a
f (PTup Sing w
_ g a1
x) = forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem ((,) j) '(w, a1) a
ISnd '(w, a1) a
ISnd -> forall (a :: k). g a -> p @@ a
f g a1
x

-- | The single-pointed universe.
instance Universe Identity where
    idecideAny :: forall k (p :: k ~> *) (as :: Identity k).
(forall (a :: k).
 Elem Identity as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any Identity p @@ as)
idecideAny forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f (SIdentity Sing n
x) =
        forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny forall {k} (b :: k). IIdentity ('Identity b) b
IId)
                    (\case WitAny Elem Identity ('Identity n) a
IIdentity ('Identity n) a
IId p @@ a
p -> p @@ a
p)
      forall a b. (a -> b) -> a -> b
$ forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f forall {k} (b :: k). IIdentity ('Identity b) b
IId Sing n
x
    idecideAll :: forall k (p :: k ~> *) (as :: Identity k).
(forall (a :: k).
 Elem Identity as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All Identity p @@ as)
idecideAll forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f (SIdentity Sing n
x) =
        forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (\Apply p n
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 b. (a -> b) -> a -> b
$ \case Elem Identity ('Identity n) a
IIdentity ('Identity n) a
IId -> Apply p n
p)
                    (\All Identity p @@ as
y -> forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Identity p @@ as
y forall {k} (b :: k). IIdentity ('Identity b) b
IId)
      forall a b. (a -> b) -> a -> b
$ forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f forall {k} (b :: k). IIdentity ('Identity b) b
IId Sing n
x
    allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All Identity p --> TyPred (Prod Identity g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f (SIdentity Sing n
x) All Identity p @@ a
a = forall {k} (a :: k -> *) (a1 :: k).
a a1 -> PIdentity a ('Identity a1)
PIdentity forall a b. (a -> b) -> a -> b
$ forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Identity p @@ a
a forall {k} (b :: k). IIdentity ('Identity b) b
IId)
    prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: Identity k).
(forall (a :: k). g a -> p @@ a)
-> Prod Identity g as -> All Identity p @@ as
prodAll forall (a :: k). g a -> p @@ a
f (PIdentity g a1
x) = forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll forall a b. (a -> b) -> a -> b
$ \case Elem Identity ('Identity a1) a
IIdentity ('Identity a1) a
IId -> forall (a :: k). g a -> p @@ a
f g a1
x