{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# 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 qualified Data.List.NonEmpty.Singletons as NE
import Data.List.Singletons hiding (
  All,
  Any,
  Elem,
  ElemSym0,
  ElemSym1,
  ElemSym2,
  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 (all, any)

-- | 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 (Decide p -> Decide (Any f p)) -> Decide p -> Decide (Any f p)
forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). 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 (Decide p -> Decide (All f p)) -> Decide p -> Decide (All f p)
forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p

instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p)

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) = Elem f a a -> (p @@ a) -> WitAny f p a
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
forall (p :: k ~> *). Provable p => Prove p
prove @p Sing a
Evident @@ a
s)

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

  -- | 'decideAll', but providing an 'Elem'.
  idecideAll ::
    forall k (p :: k ~> Type) (as :: f k).
    () =>
    -- | predicate on value
    (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
    -- | predicate on collection
    (Sing as -> Decision (All f p @@ as))

  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 =>
  -- | predicate on value
  Decide p ->
  -- | predicate on collection
  Decide (Any f p)
decideAny :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (Any f p)
decideAny Decide p
f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (Any f p) a)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
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 =>
  -- | predicate on value
  Decide p ->
  -- | predicate on collection
  Decide (All f p)
decideAll :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (All f p)
decideAll Decide p
f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (All f p) a)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
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 :: forall (f :: * -> *) k (as :: f k).
Universe f =>
Sing as -> All f (TyPred Sing) @@ as
splitSing = (forall (a :: k). Sing a -> TyCon Sing @@ a)
-> Prod f Sing as -> Apply (All f (TyCon Sing)) as
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g 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 Sing a -> Sing a
Sing a -> Apply (TyCon Sing) a
forall (a :: k). Sing a -> TyCon Sing @@ a
forall a. a -> a
id (Prod f Sing as -> WitAll f (TyCon Sing) as)
-> (Sing as -> Prod f Sing as)
-> Sing as
-> WitAll f (TyCon Sing) as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall {k} (as :: f k). 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 :: forall (f :: * -> *) k (as :: f k) (a :: k).
(Universe f, SingI as, SingI a, SDecide k) =>
Decision (Elem f as a)
pickElem =
  (WitAny f (TyPred ((:~:) a)) as -> Elem f as a)
-> (Elem f as a -> WitAny f (TyPred ((:~:) a)) as)
-> Decision (WitAny f (TyPred ((:~:) a)) as)
-> Decision (Elem f as a)
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
Elem f as a
i)
    (\case Elem f as a
i -> Elem f as a
-> (TyPred ((:~:) a) @@ a) -> WitAny f (TyPred ((:~:) a)) as
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 a :~: a
TyPred ((:~:) a) @@ a
forall {k} (a :: k). a :~: a
Refl)
    (Decision (WitAny f (TyPred ((:~:) a)) as)
 -> Decision (Elem f as a))
-> (Sing as -> Decision (WitAny f (TyPred ((:~:) a)) as))
-> Sing as
-> Decision (Elem f as a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: f k ~> *). 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 =>
  -- | always-true predicate on value
  (forall a. Elem f as a -> Sing a -> p @@ a) ->
  -- | always-true predicate on collection
  (Sing as -> All f p @@ as)
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 (a :: k). (:*:) (Elem f as) Sing a -> p @@ a)
-> Prod f (Elem f as :*: Sing) as -> Apply (All f p) as
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g 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 (\(Elem f as a
i :*: Sing a
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 Elem f as a -> Sing a -> (:*:) (Elem f as) Sing a
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 {k} (as :: f k). 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 =>
  -- | always-true predicate on value
  Prove p ->
  -- | always-true predicate on collection
  Prove (All f p)
genAll :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Prove p -> Prove (All f p)
genAll Prove p
f = Prove p -> Prod f Sing a -> Apply (All f p) a
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g 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 Sing a -> p @@ a
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 {k} (as :: f k). Sing as -> Prod f Sing as
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 (a :: k). Sing a -> Evident @@ a)
-> Prod f Sing as -> Apply (All f Evident) as
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g 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 Sing a -> Sing a
Sing a -> Apply Evident a
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 {k} (as :: f k). 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 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 -> Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as))
-> Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as)
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 Elem [] as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f Index (n1 : n2) n1
Elem [] as n1
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ Sing n1
x of
      Proved p @@ n1
p -> (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a. a -> Decision a
Proved ((Any [] p @@ as) -> Decision (Any [] p @@ as))
-> (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem [] (n1 : n2) n1 -> (p @@ n1) -> WitAny [] p (n1 : n2)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Index (n1 : n2) n1
Elem [] (n1 : n2) n1
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 (Index (n1 : n2) a -> Sing a -> Decision (Apply p a)
Elem [] as 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 Elem [] n2 a
i p @@ a
p) -> (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a. a -> Decision a
Proved ((Any [] p @@ as) -> Decision (Any [] p @@ as))
-> (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem [] (n1 : n2) a -> (p @@ a) -> WitAny [] p (n1 : n2)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
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 Index n2 a
Elem [] n2 a
i) p @@ a
p
        Disproved Refuted (Any [] p @@ n2)
vs -> Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as))
-> Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
          WitAny Index (n1 : n2) a
Elem [] (n1 : n2) a
IZ p @@ a
p -> Refuted (p @@ n1)
v p @@ n1
p @@ a
p
          WitAny (IS Index bs a
i) p @@ a
p -> Refuted (Any [] p @@ n2)
vs (Elem [] n2 a -> (p @@ a) -> WitAny [] p n2
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Index bs a
Elem [] n2 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 -> (All [] p @@ as) -> Decision (All [] p @@ as)
forall a. a -> Decision a
Proved ((All [] p @@ as) -> Decision (All [] p @@ as))
-> (All [] p @@ as) -> 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 {}
    Sing n1
x `SCons` Sing n2
xs -> case Elem [] as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f Index (n1 : n2) n1
Elem [] as n1
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 (Index (n1 : n2) a -> Sing a -> Decision (Apply p a)
Elem [] as 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 All [] p @@ n2
a -> (All [] p @@ as) -> Decision (All [] p @@ as)
forall a. a -> Decision a
Proved ((All [] p @@ as) -> Decision (All [] p @@ as))
-> (All [] p @@ as) -> 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
          Index (n1 : n2) a
Elem [] (n1 : n2) a
IZ -> p @@ n1
p @@ a
p
          IS Index bs a
i -> WitAll [] p n2 -> forall (a :: k). Elem [] n2 a -> p @@ a
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
WitAll [] p n2
a Index bs a
Elem [] n2 a
i
        Disproved Refuted (All [] p @@ n2)
v -> Refuted (All [] p @@ as) -> Decision (All [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All [] p @@ as) -> Decision (All [] p @@ as))
-> Refuted (All [] p @@ as) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \All [] p @@ as
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 (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ as
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 Refuted (p @@ n1)
v -> Refuted (All [] p @@ as) -> Decision (All [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All [] p @@ as) -> Decision (All [] p @@ as))
-> Refuted (All [] p @@ as) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \All [] p @@ as
a -> Refuted (p @@ n1)
v Refuted (p @@ n1) -> Refuted (p @@ n1)
forall a b. (a -> b) -> a -> b
$ WitAll [] p (n1 : n2)
-> forall (a :: k). Elem [] (n1 : n2) a -> p @@ a
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
WitAll [] p (n1 : n2)
a Index (n1 : n2) n1
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 {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 = Sing a -> Apply (All [] p) a -> Apply (TyCon (Prod [] g)) a
Sing a -> WitAll [] p a -> 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 :: forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go = \case
        Sing as
SList as
SNil -> \WitAll [] p as
_ -> Rec g '[]
Prod [] g as
forall {u} (a :: u -> *). Rec a '[]
RNil
        Sing n1
x `SCons` Sing n2
xs -> \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 -> forall (a :: k). Elem [] as a -> p @@ a
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 Index (n1 : n2) n1
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 (f :: * -> *) (p :: k ~> *) (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 {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 = 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 :: forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go = \case
        Rec g bs
Prod [] g bs
RNil -> (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 {}
        g r
x :& Rec g rs
xs -> (forall (a :: k). Elem [] (r : rs) a -> p @@ a)
-> WitAll [] p (r : rs)
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)
 -> WitAll [] p (r : rs))
-> (forall (a :: k). Elem [] (r : rs) a -> p @@ a)
-> WitAll [] p (r : rs)
forall a b. (a -> b) -> a -> b
$ \case
          Index (r : rs) a
Elem [] (r : rs) a
IZ -> g r -> p @@ r
forall (a :: k). g a -> p @@ a
f g r
x
          IS Index bs a
i -> WitAll [] p rs -> forall (a :: k). Elem [] rs a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (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 Rec g rs
Prod [] g rs
xs) Index bs a
Elem [] rs 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 -> Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as))
-> Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
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 Elem Maybe as n -> Sing n -> Decision (p @@ n)
forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f IJust ('Just n) n
Elem Maybe as n
forall {k} (b :: k). IJust ('Just b) b
IJust Sing n
x of
      Proved p @@ n
p -> (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a. a -> Decision a
Proved ((Any Maybe p @@ as) -> Decision (Any Maybe p @@ as))
-> (Any Maybe p @@ as) -> 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 {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny IJust ('Just n) n
Elem Maybe ('Just n) n
forall {k} (b :: k). IJust ('Just b) b
IJust p @@ n
p
      Disproved Refuted (p @@ n)
v -> Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as))
-> Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
        WitAny IJust ('Just n) a
Elem Maybe ('Just n) a
IJust p @@ a
p -> Refuted (p @@ n)
v p @@ n
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 -> (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a. a -> Decision a
Proved ((All Maybe p @@ as) -> Decision (All Maybe p @@ as))
-> (All Maybe p @@ as) -> 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 Sing n
x -> case Elem Maybe as n -> Sing n -> Decision (p @@ n)
forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f IJust ('Just n) n
Elem Maybe as n
forall {k} (b :: k). IJust ('Just b) b
IJust Sing n
x of
      Proved p @@ n
p -> (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a. a -> Decision a
Proved ((All Maybe p @@ as) -> Decision (All Maybe p @@ as))
-> (All Maybe p @@ as) -> 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 ('Just n) a
Elem Maybe ('Just n) a
IJust -> p @@ n
p @@ a
p
      Disproved Refuted (p @@ n)
v -> Refuted (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All Maybe p @@ as) -> Decision (All Maybe p @@ as))
-> Refuted (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ \All Maybe p @@ as
a -> Refuted (p @@ n)
v Refuted (p @@ n) -> Refuted (p @@ n)
forall a b. (a -> b) -> a -> b
$ WitAll Maybe p ('Just n)
-> forall (a :: k). Elem Maybe ('Just n) a -> p @@ a
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
WitAll Maybe p ('Just n)
a IJust ('Just n) n
Elem Maybe ('Just n) n
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
_ -> PMaybe g 'Nothing
TyPred (Prod Maybe g) @@ a
forall {k} (a :: k -> *). PMaybe a 'Nothing
PNothing
    SJust Sing n
x -> \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)
-> forall (a :: k). Elem Maybe ('Just n) a -> p @@ a
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
WitAll Maybe p ('Just n)
a IJust ('Just n) n
Elem Maybe ('Just n) n
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
    PMaybe g as
Prod Maybe g as
PNothing -> (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 {}
    PJust g a1
x -> (forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a)
-> WitAll Maybe p ('Just a1)
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)
 -> WitAll Maybe p ('Just a1))
-> (forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a)
-> WitAll Maybe p ('Just a1)
forall a b. (a -> b) -> a -> b
$ \case IJust ('Just a1) a
Elem Maybe ('Just a1) a
IJust -> g a1 -> p @@ a1
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
_ -> Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any (Either j) p @@ as)
 -> Decision (Any (Either j) p @@ as))
-> Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as)
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 Elem (Either j) as n -> Sing n -> Decision (p @@ n)
forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f IRight ('Right n) n
Elem (Either j) as n
forall {k} {j} (b :: k). IRight ('Right b) b
IRight Sing n
x of
      Proved p @@ n
p -> (Any (Either j) p @@ as) -> Decision (Any (Either j) p @@ as)
forall a. a -> Decision a
Proved ((Any (Either j) p @@ as) -> Decision (Any (Either j) p @@ as))
-> (Any (Either j) p @@ as) -> 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 {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny IRight ('Right n) n
Elem (Either j) ('Right n) n
forall {k} {j} (b :: k). IRight ('Right b) b
IRight p @@ n
p
      Disproved Refuted (p @@ n)
v -> Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any (Either j) p @@ as)
 -> Decision (Any (Either j) p @@ as))
-> Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
        WitAny IRight ('Right n) a
Elem (Either j) ('Right n) a
IRight p @@ a
p -> Refuted (p @@ n)
v p @@ n
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
_ -> (All (Either j) p @@ as) -> Decision (All (Either j) p @@ as)
forall a. a -> Decision a
Proved ((All (Either j) p @@ as) -> Decision (All (Either j) p @@ as))
-> (All (Either j) p @@ as) -> 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 Sing n
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 IRight ('Right n) n
Elem (Either j) as n
forall {k} {j} (b :: k). IRight ('Right b) b
IRight Sing n
x of
      Proved p @@ n
p -> (All (Either j) p @@ as) -> Decision (All (Either j) p @@ as)
forall a. a -> Decision a
Proved ((All (Either j) p @@ as) -> Decision (All (Either j) p @@ as))
-> (All (Either j) p @@ as) -> 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 ('Right n) a
Elem (Either j) ('Right n) a
IRight -> p @@ n
p @@ a
p
      Disproved Refuted (p @@ n)
v -> Refuted (All (Either j) p @@ as)
-> Decision (All (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All (Either j) p @@ as)
 -> Decision (All (Either j) p @@ as))
-> Refuted (All (Either j) p @@ as)
-> Decision (All (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \All (Either j) p @@ as
a -> Refuted (p @@ n)
v Refuted (p @@ n) -> Refuted (p @@ n)
forall a b. (a -> b) -> a -> b
$ WitAll (Either j) p ('Right n)
-> forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a
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
WitAll (Either j) p ('Right n)
a IRight ('Right n) n
Elem (Either j) ('Right n) n
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
_ -> Sing n -> PEither g ('Left n)
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 -> 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)
-> forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a
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
WitAll (Either j) p ('Right n)
a IRight ('Right n) n
Elem (Either j) ('Right n) n
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 (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> WitAll (Either j) p ('Left 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 :: k). Elem (Either j) ('Left e) a -> p @@ a)
 -> WitAll (Either j) p ('Left e))
-> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> WitAll (Either j) p ('Left e)
forall a b. (a -> b) -> a -> b
$ \case {}
    PRight g a1
x -> (forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a)
-> WitAll (Either j) p ('Right a1)
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)
 -> WitAll (Either j) p ('Right a1))
-> (forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a)
-> WitAll (Either j) p ('Right a1)
forall a b. (a -> b) -> a -> b
$ \case IRight ('Right a1) a
Elem (Either j) ('Right a1) a
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 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 Elem NonEmpty as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f NEIndex (n1 ':| n2) n1
Elem NonEmpty as n1
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead Sing n1
x of
    Proved p @@ n1
p -> (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as)
forall a. a -> Decision a
Proved ((Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as))
-> (Any NonEmpty p @@ as) -> 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 {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny NEIndex (n1 ':| n2) n1
Elem NonEmpty (n1 ':| n2) n1
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 (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a)
Elem NonEmpty as 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 Elem [] n2 a
i p @@ a
p) -> (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as)
forall a. a -> Decision a
Proved ((Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as))
-> (Any NonEmpty p @@ as) -> 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 {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
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 Index n2 a
Elem [] n2 a
i) p @@ a
p
      Disproved Refuted (Any [] p @@ n2)
vs -> Refuted (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as))
-> Refuted (Any NonEmpty p @@ as)
-> Decision (Any NonEmpty p @@ as)
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
          NEIndex (n1 ':| n2) a
Elem NonEmpty (n1 ':| n2) a
NEHead -> Refuted (p @@ n1)
v p @@ n1
p @@ a
p
          NETail Index as a
i' -> Refuted (Any [] p @@ n2)
vs (Elem [] n2 a -> (p @@ a) -> WitAny [] p n2
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Index as a
Elem [] n2 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 Elem NonEmpty as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f NEIndex (n1 ':| n2) n1
Elem NonEmpty as n1
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 (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a)
Elem NonEmpty as 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 All [] p @@ n2
ps -> (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as)
forall a. a -> Decision a
Proved ((All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as))
-> (All NonEmpty p @@ as) -> 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
        NEIndex (n1 ':| n2) a
Elem NonEmpty (n1 ':| n2) a
NEHead -> p @@ n1
p @@ a
p
        NETail Index as a
i -> WitAll [] p n2 -> forall (a :: k). Elem [] n2 a -> p @@ a
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
WitAll [] p n2
ps Index as a
Elem [] n2 a
i
      Disproved Refuted (All [] p @@ n2)
v -> Refuted (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as))
-> Refuted (All NonEmpty p @@ as)
-> Decision (All NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ \All NonEmpty p @@ as
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 (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ as
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 Refuted (p @@ n1)
v -> Refuted (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as))
-> Refuted (All NonEmpty p @@ as)
-> Decision (All NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ \All NonEmpty p @@ as
a -> Refuted (p @@ n1)
v Refuted (p @@ n1) -> Refuted (p @@ n1)
forall a b. (a -> b) -> a -> b
$ WitAll NonEmpty p (n1 ':| n2)
-> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a
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
WitAll NonEmpty p (n1 ':| n2)
a NEIndex (n1 ':| n2) n1
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 {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 =
    Sing n1 -> (p @@ n1) -> g n1
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n1
x (WitAll NonEmpty p (n1 ':| n2)
-> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a
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
WitAll NonEmpty p (n1 ':| n2)
a NEIndex (n1 ':| n2) n1
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 (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 Sing a -> (p @@ a) -> g a
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 (f :: * -> *) (p :: k ~> *) (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 {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 (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a)
-> WitAll NonEmpty p (a1 ':| 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)
 -> WitAll NonEmpty p (a1 ':| as))
-> (forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a)
-> WitAll NonEmpty p (a1 ':| as)
forall a b. (a -> b) -> a -> b
$ \case
    NEIndex (a1 ':| as) a
Elem NonEmpty (a1 ':| as) a
NEHead -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
    NETail Index as a
i -> WitAll [] p as -> forall (a :: k). Elem [] as a -> p @@ a
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 g a -> p @@ a
forall (a :: k). g a -> p @@ a
f Rec g as
Prod [] g as
xs) Index as a
Elem [] 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 Elem ((,) j) as n2 -> Sing n2 -> Decision (p @@ n2)
forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f ISnd '(n1, n2) n2
Elem ((,) j) as n2
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing n2
x of
    Proved p @@ n2
p -> (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as)
forall a. a -> Decision a
Proved ((Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as))
-> (Any ((,) j) p @@ as) -> 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 {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny ISnd '(n1, n2) n2
Elem ((,) j) '(n1, n2) n2
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd p @@ n2
p
    Disproved Refuted (p @@ n2)
v -> Refuted (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as))
-> Refuted (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \case WitAny ISnd '(n1, n2) a
Elem ((,) j) '(n1, n2) a
ISnd p @@ a
p -> Refuted (p @@ n2)
v p @@ n2
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 Elem ((,) j) as n2 -> Sing n2 -> Decision (p @@ n2)
forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f ISnd '(n1, n2) n2
Elem ((,) j) as n2
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing n2
x of
    Proved p @@ n2
p -> (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as)
forall a. a -> Decision a
Proved ((All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as))
-> (All ((,) j) p @@ as) -> 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 '(n1, n2) a
Elem ((,) j) '(n1, n2) a
ISnd -> p @@ n2
p @@ a
p
    Disproved Refuted (p @@ n2)
v -> Refuted (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as))
-> Refuted (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \All ((,) j) p @@ as
a -> Refuted (p @@ n2)
v Refuted (p @@ n2) -> Refuted (p @@ n2)
forall a b. (a -> b) -> a -> b
$ WitAll ((,) j) p '(n1, n2)
-> forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a
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
WitAll ((,) j) p '(n1, n2)
a ISnd '(n1, n2) n2
Elem ((,) j) '(n1, n2) n2
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 = 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 -> PTup g '(n1, n2)) -> g n2 -> PTup g '(n1, n2)
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)
-> forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a
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
WitAll ((,) j) p '(n1, n2)
a ISnd '(n1, n2) n2
Elem ((,) j) '(n1, n2) n2
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 (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a)
-> WitAll ((,) j) p '(w, a1)
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)
 -> WitAll ((,) j) p '(w, a1))
-> (forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a)
-> WitAll ((,) j) p '(w, a1)
forall a b. (a -> b) -> a -> b
$ \case ISnd '(w, a1) a
Elem ((,) j) '(w, a1) a
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 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) =
    (Apply p n -> Any Identity p @@ as)
-> ((Any Identity p @@ as) -> Apply p n)
-> Decision (Apply p n)
-> Decision (Any Identity p @@ as)
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 {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny IIdentity ('Identity n) n
Elem Identity ('Identity n) n
forall {k} (b :: k). IIdentity ('Identity b) b
IId)
      (\case WitAny IIdentity ('Identity n) a
Elem Identity ('Identity n) a
IId 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 IIdentity ('Identity n) n
Elem Identity as n
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) =
    (Apply p n -> All Identity p @@ as)
-> ((All Identity p @@ as) -> Apply p n)
-> Decision (Apply p n)
-> Decision (All Identity p @@ as)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision
      (\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 IIdentity ('Identity n) a
Elem Identity ('Identity n) a
IId -> Apply p n
p @@ a
p)
      (\All Identity p @@ as
y -> WitAll Identity p ('Identity n)
-> forall (a :: k). Elem Identity ('Identity n) a -> p @@ a
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
WitAll Identity p ('Identity n)
y IIdentity ('Identity n) n
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 IIdentity ('Identity n) n
Elem Identity as n
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 = g n -> PIdentity g ('Identity n)
forall {k} (a :: k -> *) (a1 :: k).
a a1 -> PIdentity a ('Identity a1)
PIdentity (g n -> PIdentity g ('Identity n))
-> g n -> PIdentity g ('Identity n)
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)
-> forall (a :: k). Elem Identity ('Identity n) a -> p @@ a
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
WitAll Identity p ('Identity n)
a IIdentity ('Identity n) n
Elem Identity ('Identity n) n
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 (a :: k). Elem Identity ('Identity a1) a -> p @@ a)
-> WitAll Identity p ('Identity a1)
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)
 -> WitAll Identity p ('Identity a1))
-> (forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a)
-> WitAll Identity p ('Identity a1)
forall a b. (a -> b) -> a -> b
$ \case IIdentity ('Identity a1) a
Elem Identity ('Identity a1) a
IId -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x