{-# 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 (
Elem, In, Universe(..)
, singAll
, Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IIdentity(..)
, All, WitAll(..), NotAll
, Any, WitAny(..), None
, Null, NotNull
, IsJust, IsNothing, IsRight, IsLeft
, decideAny, decideAll
, genAll, igenAll
, splitSing
, pickElem
) where
import Data.Functor.Identity
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Prelude hiding (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Null, Not)
import Data.Singletons.Prelude.Identity
import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import GHC.Generics ((:*:)(..))
import Prelude hiding (any, all)
import qualified Data.Singletons.Prelude.List.NonEmpty as NE
data WitAny f :: (k ~> Type) -> f k -> Type where
WitAny :: Elem f as a -> p @@ a -> WitAny f p as
data Any f :: Predicate k -> Predicate (f k)
type instance Apply (Any f p) as = WitAny f p as
newtype WitAll f p (as :: f k) = WitAll { WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll :: forall a. Elem f as a -> p @@ a }
data All f :: Predicate k -> Predicate (f k)
type instance Apply (All f p) as = WitAll f p as
instance (Universe f, Decidable p) => Decidable (Any f p) where
decide :: Sing a -> Decision (Any f p @@ a)
decide = Universe f => Decide p -> Decide (Any f p)
forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (Any f p)
decideAny @f @_ @p (Decide p -> Sing a -> Decision (Any f p @@ a))
-> Decide p -> Sing a -> Decision (Any f p @@ a)
forall a b. (a -> b) -> a -> b
$ Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p
instance (Universe f, Decidable p) => Decidable (All f p) where
decide :: Sing a -> Decision (All f p @@ a)
decide = Universe f => Decide p -> Decide (All f p)
forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (All f p)
decideAll @f @_ @p (Decide p -> Sing a -> Decision (All f p @@ a))
-> Decide p -> Sing a -> Decision (All f p @@ a)
forall a b. (a -> b) -> a -> b
$ Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p
instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p) where
instance Provable p => Provable (NotNull f ==> Any f p) where
prove :: Sing a -> (NotNull f ==> Any f p) @@ a
prove _ (WitAny i :: Elem f a a
i s :: Evident @@ a
s) = Elem f a a -> (p @@ a) -> WitAny f p a
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i (Sing a -> p @@ a
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p Sing a
Evident @@ a
s)
instance (Universe f, Provable p) => Provable (All f p) where
prove :: Sing a -> All f p @@ a
prove xs :: Sing a
xs = (forall (a :: k). Elem f a a -> p @@ a) -> All f p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem f a a -> p @@ a) -> All f p @@ a)
-> (forall (a :: k). Elem f a a -> p @@ a) -> All f p @@ a
forall a b. (a -> b) -> a -> b
$ \i :: Elem f a a
i -> Sing a -> p @@ a
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p (Elem f a a -> Sing a -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs)
instance Universe f => TFunctor (Any f) where
tmap :: (p --> q) -> Any f p --> Any f q
tmap f :: p --> q
f xs :: Sing a
xs (WitAny i x) = Elem f a a -> (q @@ a) -> WitAny f q a
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i (Sing a -> (p @@ a) -> q @@ a
p --> q
f (Elem f a a -> Sing a -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs) p @@ a
x)
instance Universe f => TFunctor (All f) where
tmap :: (p --> q) -> All f p --> All f q
tmap f :: p --> q
f xs :: Sing a
xs a :: All f p @@ a
a = (forall (a :: k1). Elem f a a -> q @@ a) -> Apply (All f q) a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k1). Elem f a a -> q @@ a) -> Apply (All f q) a)
-> (forall (a :: k1). Elem f a a -> q @@ a) -> Apply (All f q) a
forall a b. (a -> b) -> a -> b
$ \i :: Elem f a a
i -> Sing a -> (p @@ a) -> q @@ a
p --> q
f (Elem f a a -> Sing a -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs) (WitAll f p a -> Elem f a a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ a
WitAll f p a
a Elem f a a
i)
instance Universe f => DFunctor (All f) where
dmap :: (p -?> q) -> All f p -?> All f q
dmap f :: p -?> q
f xs :: Sing a
xs a :: All f p @@ a
a = (forall (a :: k1). Elem f a a -> Sing a -> Decision (q @@ a))
-> Sing a -> Decision (Apply (All f q) a)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll (\i :: Elem f a a
i x :: Sing a
x -> Sing a -> (p @@ a) -> Decision (q @@ a)
p -?> q
f Sing a
x (WitAll f p a -> Elem f a a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ a
WitAll f p a
a Elem f a a
i)) Sing a
xs
class FProd f => Universe (f :: Type -> Type) where
idecideAny
:: forall k (p :: k ~> Type) (as :: f k). ()
=> (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
-> (Sing as -> Decision (Any f p @@ as))
idecideAll
:: forall k (p :: k ~> Type) (as :: f k). ()
=> (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
-> (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
type Null f = (None f Evident :: Predicate (f k))
type NotNull f = (Any f Evident :: Predicate (f k))
type None f p = (Not (Any f p) :: Predicate (f k))
type NotAll f p = (Not (All f p) :: Predicate (f k))
decideAny
:: forall f k (p :: k ~> Type). Universe f
=> Decide p
-> Decide (Any f p)
decideAny :: Decide p -> Decide (Any f p)
decideAny f :: Decide p
f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (Any f p) a)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny ((Sing a -> Decision (Apply p a))
-> Elem f a a -> Sing a -> Decision (Apply p a)
forall a b. a -> b -> a
const Sing a -> Decision (Apply p a)
Decide p
f)
decideAll
:: forall f k (p :: k ~> Type). Universe f
=> Decide p
-> Decide (All f p)
decideAll :: Decide p -> Decide (All f p)
decideAll f :: Decide p
f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (All f p) a)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll ((Sing a -> Decision (Apply p a))
-> Elem f a a -> Sing a -> Decision (Apply p a)
forall a b. a -> b -> a
const Sing a -> Decision (Apply p a)
Decide p
f)
splitSing
:: forall f k (as :: f k). Universe f
=> Sing as
-> All f (TyPred Sing) @@ as
splitSing :: Sing as -> All f (TyPred Sing) @@ as
splitSing = (forall (a :: k). Sing a -> TyPred Sing @@ a)
-> Prod f Sing as -> All f (TyPred Sing) @@ as
forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll forall (a :: k). Sing a -> TyPred Sing @@ a
forall a. a -> a
id (Prod f Sing as -> WitAll f (TyPred Sing) as)
-> (Sing as -> Prod f Sing as)
-> Sing as
-> WitAll f (TyPred Sing) as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
pickElem
:: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k)
=> Decision (Elem f as a)
pickElem :: Decision (Elem f as a)
pickElem = (WitAny f (TyCon ((:~:) a)) as -> Elem f as a)
-> (Elem f as a -> WitAny f (TyCon ((:~:) a)) as)
-> Decision (WitAny f (TyCon ((:~:) a)) as)
-> Decision (Elem f as a)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (\case WitAny i :: Elem f as a
i Refl -> Elem f as a
Elem f as a
i)
(\case i :: Elem f as a
i -> Elem f as a
-> (TyCon ((:~:) a) @@ a) -> WitAny f (TyCon ((:~:) a)) as
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f as a
i TyCon ((:~:) a) @@ a
forall k (a :: k). a :~: a
Refl)
(Decision (WitAny f (TyCon ((:~:) a)) as)
-> Decision (Elem f as a))
-> (Sing as -> Decision (WitAny f (TyCon ((:~:) a)) as))
-> Sing as
-> Decision (Elem f as a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable (Any f (TyCon ((:~:) a))) =>
Decide (Any f (TyCon ((:~:) a)))
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @(Any f (TyPred ((:~:) a)))
(Sing as -> Decision (Elem f as a))
-> Sing as -> Decision (Elem f as a)
forall a b. (a -> b) -> a -> b
$ Sing as
forall k (a :: k). SingI a => Sing a
sing
igenAll
:: forall f k (p :: k ~> Type) (as :: f k). Universe f
=> (forall a. 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)
-> Sing as -> All f p @@ as
igenAll f :: forall (a :: k). Elem f as a -> Sing a -> p @@ a
f = (forall (a :: k). (:*:) (Elem f as) Sing a -> p @@ a)
-> Prod f (Elem f as :*: Sing) as -> All f p @@ as
forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll (\(i :*: x) -> Elem f as a -> Sing a -> p @@ a
forall (a :: k). Elem f as a -> Sing a -> p @@ a
f Elem f as a
i Sing a
x) (Prod f (Elem f as :*: Sing) as -> WitAll f p as)
-> (Sing as -> Prod f (Elem f as :*: Sing) as)
-> Sing as
-> WitAll f p as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k).
Elem f as a -> Sing a -> (:*:) (Elem f as) Sing a)
-> Prod f Sing as -> Prod f (Elem f as :*: Sing) as
forall k (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd forall (a :: k). Elem f as a -> Sing a -> (:*:) (Elem f as) Sing a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (Prod f Sing as -> Prod f (Elem f as :*: Sing) as)
-> (Sing as -> Prod f Sing as)
-> Sing as
-> Prod f (Elem f as :*: Sing) as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
genAll
:: forall f k (p :: k ~> Type). Universe f
=> Prove p
-> Prove (All f p)
genAll :: Prove p -> Prove (All f p)
genAll f :: Prove p
f = Prove p -> Prod f Sing a -> Apply (All f p) a
forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll Prove p
f (Prod f Sing a -> WitAll f p a)
-> (Sing a -> Prod f Sing a) -> Sing a -> WitAll f p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod f Sing a
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
singAll
:: forall f k (as :: f k). Universe f
=> Sing as
-> All f Evident @@ as
singAll :: Sing as -> All f Evident @@ as
singAll = (forall (a :: k). Sing a -> Evident @@ a)
-> Prod f Sing as -> All f Evident @@ as
forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll forall (a :: k). Sing a -> Evident @@ a
forall a. a -> a
id (Prod f Sing as -> WitAll f Evident as)
-> (Sing as -> Prod f Sing as) -> Sing as -> WitAll f Evident as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
type IsJust = (NotNull Maybe :: Predicate (Maybe k))
type IsNothing = (Null Maybe :: Predicate (Maybe k))
type IsRight = (NotNull (Either j) :: Predicate (Either j k))
type IsLeft = (Null (Either j) :: Predicate (Either j k))
instance Universe [] where
idecideAny
:: forall k (p :: k ~> Type) (as :: [k]). ()
=> (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Decision (Any [] p @@ as)
idecideAny :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any [] p @@ as)
idecideAny f :: forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f = \case
SNil -> Refuted (WitAny [] p '[]) -> Decision (Any [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAny [] p '[]) -> Decision (Any [] p @@ as))
-> Refuted (WitAny [] p '[]) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny i :: Elem [] '[] a
i _ -> case Elem [] '[] a
i of {}
x `SCons` xs -> case Elem [] as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f Elem [] as n1
forall k (b :: k) (as :: [k]). Index (b : as) b
IZ Sing n1
x of
Proved p :: p @@ n1
p -> WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as)
forall a. a -> Decision a
Proved (WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as))
-> WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem [] (n1 : n2) n1 -> (p @@ n1) -> WitAny [] p (n1 : n2)
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem [] (n1 : n2) n1
forall k (b :: k) (as :: [k]). Index (b : as) b
IZ p @@ n1
p
Disproved v :: Refuted (p @@ n1)
v -> case (forall (a :: k). Elem [] n2 a -> Sing a -> Decision (p @@ a))
-> Sing n2 -> Decision (Any [] p @@ n2)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny @[] @_ @p (Index (n1 : n2) a -> Sing a -> Decision (Apply p a)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f (Index (n1 : n2) a -> Sing a -> Decision (Apply p a))
-> (Index n2 a -> Index (n1 : n2) a)
-> Index n2 a
-> Sing a
-> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> Index (n1 : n2) a
forall k (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS) Sing n2
xs of
Proved (WitAny i p) -> WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as)
forall a. a -> Decision a
Proved (WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as))
-> WitAny [] p (n1 : n2) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem [] (n1 : n2) a -> (p @@ a) -> WitAny [] p (n1 : n2)
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny (Index n2 a -> Index (n1 : n2) a
forall k (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Elem [] n2 a
Index n2 a
i) p @@ a
p
Disproved vs :: Refuted (Any [] p @@ n2)
vs -> Refuted (WitAny [] p (n1 : n2)) -> Decision (Any [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAny [] p (n1 : n2)) -> Decision (Any [] p @@ as))
-> Refuted (WitAny [] p (n1 : n2)) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny IZ p :: p @@ a
p -> Refuted (p @@ n1)
v p @@ n1
p @@ a
p
WitAny (IS i) p :: p @@ a
p -> Refuted (Any [] p @@ n2)
vs (Elem [] n2 a -> (p @@ a) -> WitAny [] p n2
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem [] n2 a
Index bs a
i p @@ a
p)
idecideAll
:: forall k (p :: k ~> Type) (as :: [k]). ()
=> (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Decision (All [] p @@ as)
idecideAll :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All [] p @@ as)
idecideAll f :: forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f = \case
SNil -> WitAll [] p '[] -> Decision (All [] p @@ as)
forall a. a -> Decision a
Proved (WitAll [] p '[] -> Decision (All [] p @@ as))
-> WitAll [] p '[] -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[])
-> (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]
forall a b. (a -> b) -> a -> b
$ \case {}
x `SCons` xs -> case Elem [] as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f Elem [] as n1
forall k (b :: k) (as :: [k]). Index (b : as) b
IZ Sing n1
x of
Proved p :: p @@ n1
p -> case (forall (a :: k). Elem [] n2 a -> Sing a -> Decision (p @@ a))
-> Sing n2 -> Decision (All [] p @@ n2)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll @[] @_ @p (Index (n1 : n2) a -> Sing a -> Decision (Apply p a)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f (Index (n1 : n2) a -> Sing a -> Decision (Apply p a))
-> (Index n2 a -> Index (n1 : n2) a)
-> Index n2 a
-> Sing a
-> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> Index (n1 : n2) a
forall k (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS) Sing n2
xs of
Proved a :: All [] p @@ n2
a -> WitAll [] p (n1 : n2) -> Decision (All [] p @@ as)
forall a. a -> Decision a
Proved (WitAll [] p (n1 : n2) -> Decision (All [] p @@ as))
-> WitAll [] p (n1 : n2) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem [] (n1 : n2) a -> p @@ a)
-> WitAll [] p (n1 : n2)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] (n1 : n2) a -> p @@ a)
-> WitAll [] p (n1 : n2))
-> (forall (a :: k). Elem [] (n1 : n2) a -> p @@ a)
-> WitAll [] p (n1 : n2)
forall a b. (a -> b) -> a -> b
$ \case
IZ -> p @@ n1
Apply p a
p
IS i -> WitAll [] p n2 -> Elem [] n2 a -> Apply p a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ n2
WitAll [] p n2
a Elem [] n2 a
Index bs a
i
Disproved v :: Refuted (All [] p @@ n2)
v -> Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as))
-> Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \a :: WitAll [] p (n1 : n2)
a -> Refuted (All [] p @@ n2)
v Refuted (All [] p @@ n2) -> Refuted (All [] p @@ n2)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (WitAll [] p (n1 : n2)
-> forall (a :: k). Elem [] (n1 : n2) a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll [] p (n1 : n2)
a (Index (n1 : n2) a -> Apply p a)
-> (Index n2 a -> Index (n1 : n2) a) -> Index n2 a -> Apply p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> Index (n1 : n2) a
forall k (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS)
Disproved v :: Refuted (p @@ n1)
v -> Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as))
-> Refuted (WitAll [] p (n1 : n2)) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \a :: WitAll [] p (n1 : n2)
a -> Refuted (p @@ n1)
v Refuted (p @@ n1) -> Refuted (p @@ n1)
forall a b. (a -> b) -> a -> b
$ WitAll [] p (n1 : n2) -> Elem [] (n1 : n2) n1 -> p @@ n1
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll [] p (n1 : n2)
a Elem [] (n1 : n2) n1
forall k (b :: k) (as :: [k]). Index (b : as) b
IZ
allProd
:: forall p g. ()
=> (forall a. Sing a -> p @@ a -> g a)
-> All [] p --> TyPred (Prod [] g)
allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All [] p --> TyPred (Prod [] g)
allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a
f = Sing a -> Apply (All [] p) a -> Apply (TyPred (Prod [] g)) a
forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go
where
go :: Sing as -> WitAll [] p as -> Prod [] g as
go :: Sing as -> WitAll [] p as -> Prod [] g as
go = \case
SNil -> \_ -> Prod [] g as
forall u (a :: u -> *). Rec a '[]
RNil
x `SCons` xs -> \a :: WitAll [] p as
a -> Sing n1 -> (p @@ n1) -> g n1
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n1
x (WitAll [] p as -> Elem [] as n1 -> p @@ n1
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll [] p as
a Elem [] as n1
forall k (b :: k) (as :: [k]). Index (b : as) b
IZ)
g n1 -> Rec g n2 -> Rec g (n1 : n2)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing n2 -> WitAll [] p n2 -> Prod [] g n2
forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go Sing n2
xs ((forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (WitAll [] p as -> forall (a :: k). Elem [] as a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll [] p as
a (Index (n1 : n2) a -> Apply p a)
-> (Index n2 a -> Index (n1 : n2) a) -> Index n2 a -> Apply p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> Index (n1 : n2) a
forall k (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS))
prodAll
:: forall p g as. ()
=> (forall a. g a -> p @@ a)
-> Prod [] g as
-> All [] p @@ as
prodAll :: (forall (a :: k). g a -> p @@ a) -> Prod [] g as -> All [] p @@ as
prodAll f :: forall (a :: k). g a -> p @@ a
f = Prod [] g as -> All [] p @@ as
forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go
where
go :: Prod [] g bs -> All [] p @@ bs
go :: Prod [] g bs -> All [] p @@ bs
go = \case
RNil -> (forall (a :: k). Elem [] '[] a -> p @@ a) -> All [] p @@ bs
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] '[] a -> p @@ a) -> All [] p @@ bs)
-> (forall (a :: k). Elem [] '[] a -> p @@ a) -> All [] p @@ bs
forall a b. (a -> b) -> a -> b
$ \case {}
x :& xs -> (forall (a :: k). Elem [] (r : rs) a -> p @@ a) -> All [] p @@ bs
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] (r : rs) a -> p @@ a) -> All [] p @@ bs)
-> (forall (a :: k). Elem [] (r : rs) a -> p @@ a)
-> All [] p @@ bs
forall a b. (a -> b) -> a -> b
$ \case
IZ -> g r -> p @@ r
forall (a :: k). g a -> p @@ a
f g r
x
IS i -> WitAll [] p rs -> Elem [] rs a -> Apply p a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (Prod [] g rs -> All [] p @@ rs
forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go Prod [] g rs
Rec g rs
xs) Elem [] rs a
Index bs a
i
instance Universe Maybe where
idecideAny :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any Maybe p @@ as)
idecideAny f :: forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f = \case
SNothing -> Refuted (WitAny Maybe p 'Nothing) -> Decision (Any Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAny Maybe p 'Nothing) -> Decision (Any Maybe p @@ as))
-> Refuted (WitAny Maybe p 'Nothing)
-> Decision (Any Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ \case WitAny i :: Elem Maybe 'Nothing a
i _ -> case Elem Maybe 'Nothing a
i of {}
SJust x -> case Elem Maybe as n -> Sing n -> Decision (p @@ n)
forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f Elem Maybe as n
forall k (b :: k). IJust ('Just b) b
IJust Sing n
x of
Proved p :: p @@ n
p -> WitAny Maybe p ('Just n) -> Decision (Any Maybe p @@ as)
forall a. a -> Decision a
Proved (WitAny Maybe p ('Just n) -> Decision (Any Maybe p @@ as))
-> WitAny Maybe p ('Just n) -> Decision (Any Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem Maybe ('Just n) n -> (p @@ n) -> WitAny Maybe p ('Just n)
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem Maybe ('Just n) n
forall k (b :: k). IJust ('Just b) b
IJust p @@ n
p
Disproved v :: Refuted (p @@ n)
v -> Refuted (WitAny Maybe p ('Just n)) -> Decision (Any Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAny Maybe p ('Just n))
-> Decision (Any Maybe p @@ as))
-> Refuted (WitAny Maybe p ('Just n))
-> Decision (Any Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny IJust p :: p @@ a
p -> Refuted (p @@ n)
v p @@ n
p @@ a
p
idecideAll :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All Maybe p @@ as)
idecideAll f :: forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f = \case
SNothing -> WitAll Maybe p 'Nothing -> Decision (All Maybe p @@ as)
forall a. a -> Decision a
Proved (WitAll Maybe p 'Nothing -> Decision (All Maybe p @@ as))
-> WitAll Maybe p 'Nothing -> Decision (All Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing)
-> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing
forall a b. (a -> b) -> a -> b
$ \case {}
SJust x -> case Elem Maybe as n -> Sing n -> Decision (p @@ n)
forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f Elem Maybe as n
forall k (b :: k). IJust ('Just b) b
IJust Sing n
x of
Proved p :: p @@ n
p -> WitAll Maybe p ('Just n) -> Decision (All Maybe p @@ as)
forall a. a -> Decision a
Proved (WitAll Maybe p ('Just n) -> Decision (All Maybe p @@ as))
-> WitAll Maybe p ('Just n) -> Decision (All Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem Maybe ('Just n) a -> p @@ a)
-> WitAll Maybe p ('Just n)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe ('Just n) a -> p @@ a)
-> WitAll Maybe p ('Just n))
-> (forall (a :: k). Elem Maybe ('Just n) a -> p @@ a)
-> WitAll Maybe p ('Just n)
forall a b. (a -> b) -> a -> b
$ \case IJust -> p @@ n
Apply p a
p
Disproved v :: Refuted (p @@ n)
v -> Refuted (WitAll Maybe p ('Just n)) -> Decision (All Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAll Maybe p ('Just n))
-> Decision (All Maybe p @@ as))
-> Refuted (WitAll Maybe p ('Just n))
-> Decision (All Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ \a :: WitAll Maybe p ('Just n)
a -> Refuted (p @@ n)
v Refuted (p @@ n) -> Refuted (p @@ n)
forall a b. (a -> b) -> a -> b
$ WitAll Maybe p ('Just n) -> Elem Maybe ('Just n) n -> p @@ n
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll Maybe p ('Just n)
a Elem Maybe ('Just n) n
forall k (b :: k). IJust ('Just b) b
IJust
allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All Maybe p --> TyPred (Prod Maybe g)
allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a
f = \case
SNothing -> \_ -> Apply (TyPred (Prod Maybe g)) a
forall k (a :: k -> *). PMaybe a 'Nothing
PNothing
SJust x -> \a :: All Maybe p @@ a
a -> g n -> PMaybe g ('Just n)
forall k (a :: k -> *) (a1 :: k). a a1 -> PMaybe a ('Just a1)
PJust (Sing n -> (p @@ n) -> g n
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (WitAll Maybe p ('Just n) -> Elem Maybe ('Just n) n -> p @@ n
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Maybe p @@ a
WitAll Maybe p ('Just n)
a Elem Maybe ('Just n) n
forall k (b :: k). IJust ('Just b) b
IJust))
prodAll :: (forall (a :: k). g a -> p @@ a)
-> Prod Maybe g as -> All Maybe p @@ as
prodAll f :: forall (a :: k). g a -> p @@ a
f = \case
PNothing -> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> All Maybe p @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> All Maybe p @@ as)
-> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> All Maybe p @@ as
forall a b. (a -> b) -> a -> b
$ \case {}
PJust x -> (forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a)
-> All Maybe p @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a)
-> All Maybe p @@ as)
-> (forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a)
-> All Maybe p @@ as
forall a b. (a -> b) -> a -> b
$ \case IJust -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
instance Universe (Either j) where
idecideAny :: (forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any (Either j) p @@ as)
idecideAny f :: forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f = \case
SLeft _ -> Refuted (WitAny (Either j) p ('Left n))
-> Decision (Any (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAny (Either j) p ('Left n))
-> Decision (Any (Either j) p @@ as))
-> Refuted (WitAny (Either j) p ('Left n))
-> Decision (Any (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \case WitAny i :: Elem (Either j) ('Left n) a
i _ -> case Elem (Either j) ('Left n) a
i of {}
SRight x -> case Elem (Either j) as n -> Sing n -> Decision (p @@ n)
forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f Elem (Either j) as n
forall k j (b :: k). IRight ('Right b) b
IRight Sing n
x of
Proved p :: p @@ n
p -> WitAny (Either j) p ('Right n) -> Decision (Any (Either j) p @@ as)
forall a. a -> Decision a
Proved (WitAny (Either j) p ('Right n)
-> Decision (Any (Either j) p @@ as))
-> WitAny (Either j) p ('Right n)
-> Decision (Any (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem (Either j) ('Right n) n
-> (p @@ n) -> WitAny (Either j) p ('Right n)
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem (Either j) ('Right n) n
forall k j (b :: k). IRight ('Right b) b
IRight p @@ n
p
Disproved v :: Refuted (p @@ n)
v -> Refuted (WitAny (Either j) p ('Right n))
-> Decision (Any (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAny (Either j) p ('Right n))
-> Decision (Any (Either j) p @@ as))
-> Refuted (WitAny (Either j) p ('Right n))
-> Decision (Any (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny IRight p :: p @@ a
p -> Refuted (p @@ n)
v p @@ n
p @@ a
p
idecideAll :: (forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All (Either j) p @@ as)
idecideAll f :: forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f = \case
SLeft _ -> WitAll (Either j) p ('Left n) -> Decision (All (Either j) p @@ as)
forall a. a -> Decision a
Proved (WitAll (Either j) p ('Left n)
-> Decision (All (Either j) p @@ as))
-> WitAll (Either j) p ('Left n)
-> Decision (All (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a)
-> WitAll (Either j) p ('Left n)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a)
-> WitAll (Either j) p ('Left n))
-> (forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a)
-> WitAll (Either j) p ('Left n)
forall a b. (a -> b) -> a -> b
$ \case {}
SRight x -> case Elem (Either j) as n -> Sing n -> Decision (p @@ n)
forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f Elem (Either j) as n
forall k j (b :: k). IRight ('Right b) b
IRight Sing n
x of
Proved p :: p @@ n
p -> WitAll (Either j) p ('Right n) -> Decision (All (Either j) p @@ as)
forall a. a -> Decision a
Proved (WitAll (Either j) p ('Right n)
-> Decision (All (Either j) p @@ as))
-> WitAll (Either j) p ('Right n)
-> Decision (All (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a)
-> WitAll (Either j) p ('Right n)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a)
-> WitAll (Either j) p ('Right n))
-> (forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a)
-> WitAll (Either j) p ('Right n)
forall a b. (a -> b) -> a -> b
$ \case IRight -> p @@ n
Apply p a
p
Disproved v :: Refuted (p @@ n)
v -> Refuted (WitAll (Either j) p ('Right n))
-> Decision (All (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAll (Either j) p ('Right n))
-> Decision (All (Either j) p @@ as))
-> Refuted (WitAll (Either j) p ('Right n))
-> Decision (All (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \a :: WitAll (Either j) p ('Right n)
a -> Refuted (p @@ n)
v Refuted (p @@ n) -> Refuted (p @@ n)
forall a b. (a -> b) -> a -> b
$ WitAll (Either j) p ('Right n)
-> Elem (Either j) ('Right n) n -> p @@ n
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll (Either j) p ('Right n)
a Elem (Either j) ('Right n) n
forall k j (b :: k). IRight ('Right b) b
IRight
allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All (Either j) p --> TyPred (Prod (Either j) g)
allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a
f = \case
SLeft w -> \_ -> Sing n -> PEither g ('Left n)
forall j k (e :: j) (a :: k -> *). Sing e -> PEither a ('Left e)
PLeft Sing n
w
SRight x -> \a :: All (Either j) p @@ a
a -> g n -> PEither g ('Right n)
forall k j (a :: k -> *) (a1 :: k). a a1 -> PEither a ('Right a1)
PRight (Sing n -> (p @@ n) -> g n
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (WitAll (Either j) p ('Right n)
-> Elem (Either j) ('Right n) n -> p @@ n
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All (Either j) p @@ a
WitAll (Either j) p ('Right n)
a Elem (Either j) ('Right n) n
forall k j (b :: k). IRight ('Right b) b
IRight))
prodAll :: (forall (a :: k). g a -> p @@ a)
-> Prod (Either j) g as -> All (Either j) p @@ as
prodAll f :: forall (a :: k). g a -> p @@ a
f = \case
PLeft _ -> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> All (Either j) p @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> All (Either j) p @@ as)
-> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> All (Either j) p @@ as
forall a b. (a -> b) -> a -> b
$ \case {}
PRight x -> (forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a)
-> All (Either j) p @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a)
-> All (Either j) p @@ as)
-> (forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a)
-> All (Either j) p @@ as
forall a b. (a -> b) -> a -> b
$ \case IRight -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
instance Universe NonEmpty where
idecideAny
:: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
=> (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Decision (Any NonEmpty p @@ as)
idecideAny :: (forall (a :: k).
Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any NonEmpty p @@ as)
idecideAny f :: forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f (x NE.:%| xs) = case Elem NonEmpty as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f Elem NonEmpty as n1
forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead Sing n1
x of
Proved p :: p @@ n1
p -> WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as)
forall a. a -> Decision a
Proved (WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as))
-> WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem NonEmpty (n1 ':| n2) n1
-> (p @@ n1) -> WitAny NonEmpty p (n1 ':| n2)
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem NonEmpty (n1 ':| n2) n1
forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead p @@ n1
p
Disproved v :: Refuted (p @@ n1)
v -> case (forall (a :: k). Elem [] n2 a -> Sing a -> Decision (p @@ a))
-> Sing n2 -> Decision (Any [] p @@ n2)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny @[] @_ @p (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a))
-> (Index n2 a -> NEIndex (n1 ':| n2) a)
-> Index n2 a
-> Sing a
-> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> NEIndex (n1 ':| n2) a
forall k (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail) Sing n2
xs of
Proved (WitAny i p) -> WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as)
forall a. a -> Decision a
Proved (WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as))
-> WitAny NonEmpty p (n1 ':| n2) -> Decision (Any NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem NonEmpty (n1 ':| n2) a
-> (p @@ a) -> WitAny NonEmpty p (n1 ':| n2)
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny (Index n2 a -> NEIndex (n1 ':| n2) a
forall k (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail Elem [] n2 a
Index n2 a
i) p @@ a
p
Disproved vs :: Refuted (Any [] p @@ n2)
vs -> Refuted (WitAny NonEmpty p (n1 ':| n2))
-> Decision (Any NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAny NonEmpty p (n1 ':| n2))
-> Decision (Any NonEmpty p @@ as))
-> Refuted (WitAny NonEmpty p (n1 ':| n2))
-> Decision (Any NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny i :: Elem NonEmpty (n1 ':| n2) a
i p :: p @@ a
p -> case Elem NonEmpty (n1 ':| n2) a
i of
NEHead -> Refuted (p @@ n1)
v p @@ n1
p @@ a
p
NETail i' -> Refuted (Any [] p @@ n2)
vs (Elem [] n2 a -> (p @@ a) -> WitAny [] p n2
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem [] n2 a
Index as a
i' p @@ a
p)
idecideAll
:: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
=> (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
-> Sing as
-> Decision (All NonEmpty p @@ as)
idecideAll :: (forall (a :: k).
Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All NonEmpty p @@ as)
idecideAll f :: forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f (x NE.:%| xs) = case Elem NonEmpty as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f Elem NonEmpty as n1
forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead Sing n1
x of
Proved p :: p @@ n1
p -> case (forall (a :: k). Elem [] n2 a -> Sing a -> Decision (p @@ a))
-> Sing n2 -> Decision (All [] p @@ n2)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll @[] @_ @p (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a))
-> (Index n2 a -> NEIndex (n1 ':| n2) a)
-> Index n2 a
-> Sing a
-> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> NEIndex (n1 ':| n2) a
forall k (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail) Sing n2
xs of
Proved ps :: All [] p @@ n2
ps -> WitAll NonEmpty p (n1 ':| n2) -> Decision (All NonEmpty p @@ as)
forall a. a -> Decision a
Proved (WitAll NonEmpty p (n1 ':| n2) -> Decision (All NonEmpty p @@ as))
-> WitAll NonEmpty p (n1 ':| n2) -> Decision (All NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a)
-> WitAll NonEmpty p (n1 ':| n2)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a)
-> WitAll NonEmpty p (n1 ':| n2))
-> (forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a)
-> WitAll NonEmpty p (n1 ':| n2)
forall a b. (a -> b) -> a -> b
$ \case
NEHead -> p @@ n1
Apply p a
p
NETail i -> WitAll [] p n2 -> Elem [] n2 a -> Apply p a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ n2
WitAll [] p n2
ps Elem [] n2 a
Index as a
i
Disproved v :: Refuted (All [] p @@ n2)
v -> Refuted (WitAll NonEmpty p (n1 ':| n2))
-> Decision (All NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAll NonEmpty p (n1 ':| n2))
-> Decision (All NonEmpty p @@ as))
-> Refuted (WitAll NonEmpty p (n1 ':| n2))
-> Decision (All NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ \a :: WitAll NonEmpty p (n1 ':| n2)
a -> Refuted (All [] p @@ n2)
v Refuted (All [] p @@ n2) -> Refuted (All [] p @@ n2)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (WitAll NonEmpty p (n1 ':| n2)
-> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll NonEmpty p (n1 ':| n2)
a (NEIndex (n1 ':| n2) a -> Apply p a)
-> (Index n2 a -> NEIndex (n1 ':| n2) a) -> Index n2 a -> Apply p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> NEIndex (n1 ':| n2) a
forall k (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail)
Disproved v :: Refuted (p @@ n1)
v -> Refuted (WitAll NonEmpty p (n1 ':| n2))
-> Decision (All NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAll NonEmpty p (n1 ':| n2))
-> Decision (All NonEmpty p @@ as))
-> Refuted (WitAll NonEmpty p (n1 ':| n2))
-> Decision (All NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ \a :: WitAll NonEmpty p (n1 ':| n2)
a -> Refuted (p @@ n1)
v Refuted (p @@ n1) -> Refuted (p @@ n1)
forall a b. (a -> b) -> a -> b
$ WitAll NonEmpty p (n1 ':| n2)
-> Elem NonEmpty (n1 ':| n2) n1 -> p @@ n1
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll NonEmpty p (n1 ':| n2)
a Elem NonEmpty (n1 ':| n2) n1
forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead
allProd
:: forall p g. ()
=> (forall a. Sing a -> p @@ a -> g a)
-> All NonEmpty p --> TyPred (Prod NonEmpty g)
allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All NonEmpty p --> TyPred (Prod NonEmpty g)
allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a
f (x NE.:%| xs) a :: All NonEmpty p @@ a
a =
Sing n1 -> (p @@ n1) -> g n1
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n1
x (WitAll NonEmpty p (n1 ':| n2)
-> Elem NonEmpty (n1 ':| n2) n1 -> p @@ n1
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ a
WitAll NonEmpty p (n1 ':| n2)
a Elem NonEmpty (n1 ':| n2) n1
forall k (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead)
g n1 -> Rec g n2 -> NERec g (n1 ':| n2)
forall k (a :: k -> *) (a1 :: k) (as :: [k]).
a a1 -> Rec a as -> NERec a (a1 ':| as)
:&| (forall (a :: k). Sing a -> (p @@ a) -> g a)
-> Sing n2 -> (All [] p @@ n2) -> TyPred (Prod [] g) @@ n2
forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *).
Universe f =>
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All f p --> TyPred (Prod f g)
allProd @[] @p forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n2
xs ((forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (WitAll NonEmpty p (n1 ':| n2)
-> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ a
WitAll NonEmpty p (n1 ':| n2)
a (NEIndex (n1 ':| n2) a -> Apply p a)
-> (Index n2 a -> NEIndex (n1 ':| n2) a) -> Index n2 a -> Apply p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> NEIndex (n1 ':| n2) a
forall k (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail))
prodAll
:: forall p g as. ()
=> (forall a. g a -> p @@ a)
-> Prod NonEmpty g as
-> All NonEmpty p @@ as
prodAll :: (forall (a :: k). g a -> p @@ a)
-> Prod NonEmpty g as -> All NonEmpty p @@ as
prodAll f :: forall (a :: k). g a -> p @@ a
f (x :&| xs) = (forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a)
-> All NonEmpty p @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a)
-> All NonEmpty p @@ as)
-> (forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a)
-> All NonEmpty p @@ as
forall a b. (a -> b) -> a -> b
$ \case
NEHead -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
NETail i -> WitAll [] p as -> Elem [] as a -> Apply p a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll ((forall (a :: k). g a -> p @@ a) -> Prod [] g as -> All [] p @@ as
forall (f :: * -> *) k (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll @[] @p forall (a :: k). g a -> p @@ a
f Prod [] g as
Rec g as
xs) Elem [] as a
Index as a
i
instance Universe ((,) j) where
idecideAny :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any ((,) j) p @@ as)
idecideAny f :: forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f (STuple2 _ x) = case Elem ((,) j) as n2 -> Sing n2 -> Decision (p @@ n2)
forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f Elem ((,) j) as n2
forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing n2
x of
Proved p :: p @@ n2
p -> WitAny ((,) j) p '(n1, n2) -> Decision (Any ((,) j) p @@ as)
forall a. a -> Decision a
Proved (WitAny ((,) j) p '(n1, n2) -> Decision (Any ((,) j) p @@ as))
-> WitAny ((,) j) p '(n1, n2) -> Decision (Any ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem ((,) j) '(n1, n2) n2
-> (p @@ n2) -> WitAny ((,) j) p '(n1, n2)
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem ((,) j) '(n1, n2) n2
forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd p @@ n2
p
Disproved v :: Refuted (p @@ n2)
v -> Refuted (WitAny ((,) j) p '(n1, n2))
-> Decision (Any ((,) j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAny ((,) j) p '(n1, n2))
-> Decision (Any ((,) j) p @@ as))
-> Refuted (WitAny ((,) j) p '(n1, n2))
-> Decision (Any ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \case WitAny ISnd p :: p @@ a
p -> Refuted (p @@ n2)
v p @@ n2
p @@ a
p
idecideAll :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All ((,) j) p @@ as)
idecideAll f :: forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f (STuple2 _ x) = case Elem ((,) j) as n2 -> Sing n2 -> Decision (p @@ n2)
forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f Elem ((,) j) as n2
forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing n2
x of
Proved p :: p @@ n2
p -> WitAll ((,) j) p '(n1, n2) -> Decision (All ((,) j) p @@ as)
forall a. a -> Decision a
Proved (WitAll ((,) j) p '(n1, n2) -> Decision (All ((,) j) p @@ as))
-> WitAll ((,) j) p '(n1, n2) -> Decision (All ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a)
-> WitAll ((,) j) p '(n1, n2)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a)
-> WitAll ((,) j) p '(n1, n2))
-> (forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a)
-> WitAll ((,) j) p '(n1, n2)
forall a b. (a -> b) -> a -> b
$ \case ISnd -> p @@ n2
Apply p a
p
Disproved v :: Refuted (p @@ n2)
v -> Refuted (WitAll ((,) j) p '(n1, n2))
-> Decision (All ((,) j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (WitAll ((,) j) p '(n1, n2))
-> Decision (All ((,) j) p @@ as))
-> Refuted (WitAll ((,) j) p '(n1, n2))
-> Decision (All ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \a :: WitAll ((,) j) p '(n1, n2)
a -> Refuted (p @@ n2)
v Refuted (p @@ n2) -> Refuted (p @@ n2)
forall a b. (a -> b) -> a -> b
$ WitAll ((,) j) p '(n1, n2) -> Elem ((,) j) '(n1, n2) n2 -> p @@ n2
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll ((,) j) p '(n1, n2)
a Elem ((,) j) '(n1, n2) n2
forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd
allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All ((,) j) p --> TyPred (Prod ((,) j) g)
allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a
f (STuple2 w x) a :: All ((,) j) p @@ a
a = Sing n1 -> g n2 -> PTup g '(n1, n2)
forall j k (w :: j) (a :: k -> *) (a1 :: k).
Sing w -> a a1 -> PTup a '(w, a1)
PTup Sing n1
w (g n2 -> Apply (TyPred (Prod ((,) j) g)) a)
-> g n2 -> Apply (TyPred (Prod ((,) j) g)) a
forall a b. (a -> b) -> a -> b
$ Sing n2 -> (p @@ n2) -> g n2
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n2
x (WitAll ((,) j) p '(n1, n2) -> Elem ((,) j) '(n1, n2) n2 -> p @@ n2
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All ((,) j) p @@ a
WitAll ((,) j) p '(n1, n2)
a Elem ((,) j) '(n1, n2) n2
forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd)
prodAll :: (forall (a :: k). g a -> p @@ a)
-> Prod ((,) j) g as -> All ((,) j) p @@ as
prodAll f :: forall (a :: k). g a -> p @@ a
f (PTup _ x) = (forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a)
-> All ((,) j) p @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a)
-> All ((,) j) p @@ as)
-> (forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a)
-> All ((,) j) p @@ as
forall a b. (a -> b) -> a -> b
$ \case ISnd -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
instance Universe Identity where
idecideAny :: (forall (a :: k).
Elem Identity as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any Identity p @@ as)
idecideAny f :: forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f (SIdentity x) =
(Apply p n -> WitAny Identity p ('Identity n))
-> (WitAny Identity p ('Identity n) -> Apply p n)
-> Decision (Apply p n)
-> Decision (WitAny Identity p ('Identity n))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Elem Identity ('Identity n) n
-> Apply p n -> WitAny Identity p ('Identity n)
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem Identity ('Identity n) n
forall k (b :: k). IIdentity ('Identity b) b
IId)
(\case WitAny IId p :: p @@ a
p -> Apply p n
p @@ a
p)
(Decision (Apply p n) -> Decision (Any Identity p @@ as))
-> Decision (Apply p n) -> Decision (Any Identity p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem Identity as n -> Sing n -> Decision (Apply p n)
forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f Elem Identity as n
forall k (b :: k). IIdentity ('Identity b) b
IId Sing n
x
idecideAll :: (forall (a :: k).
Elem Identity as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All Identity p @@ as)
idecideAll f :: forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f (SIdentity x) =
(Apply p n -> WitAll Identity p ('Identity n))
-> (WitAll Identity p ('Identity n) -> Apply p n)
-> Decision (Apply p n)
-> Decision (WitAll Identity p ('Identity n))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (\p :: Apply p n
p -> (forall (a :: k). Elem Identity ('Identity n) a -> p @@ a)
-> WitAll Identity p ('Identity n)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Identity ('Identity n) a -> p @@ a)
-> WitAll Identity p ('Identity n))
-> (forall (a :: k). Elem Identity ('Identity n) a -> p @@ a)
-> WitAll Identity p ('Identity n)
forall a b. (a -> b) -> a -> b
$ \case IId -> Apply p n
Apply p a
p)
(WitAll Identity p ('Identity n)
-> Elem Identity ('Identity n) n -> Apply p n
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
`runWitAll` Elem Identity ('Identity n) n
forall k (b :: k). IIdentity ('Identity b) b
IId)
(Decision (Apply p n) -> Decision (All Identity p @@ as))
-> Decision (Apply p n) -> Decision (All Identity p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem Identity as n -> Sing n -> Decision (Apply p n)
forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f Elem Identity as n
forall k (b :: k). IIdentity ('Identity b) b
IId Sing n
x
allProd :: (forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All Identity p --> TyPred (Prod Identity g)
allProd f :: forall (a :: k). Sing a -> (p @@ a) -> g a
f (SIdentity x) a :: All Identity p @@ a
a = g n -> Apply (TyPred (Prod Identity g)) a
forall k (a :: k -> *) (a1 :: k).
a a1 -> PIdentity a ('Identity a1)
PIdentity (g n -> Apply (TyPred (Prod Identity g)) a)
-> g n -> Apply (TyPred (Prod Identity g)) a
forall a b. (a -> b) -> a -> b
$ Sing n -> (p @@ n) -> g n
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (WitAll Identity p ('Identity n)
-> Elem Identity ('Identity n) n -> p @@ n
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Identity p @@ a
WitAll Identity p ('Identity n)
a Elem Identity ('Identity n) n
forall k (b :: k). IIdentity ('Identity b) b
IId)
prodAll :: (forall (a :: k). g a -> p @@ a)
-> Prod Identity g as -> All Identity p @@ as
prodAll f :: forall (a :: k). g a -> p @@ a
f (PIdentity x) = (forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a)
-> All Identity p @@ as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a)
-> All Identity p @@ as)
-> (forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a)
-> All Identity p @@ as
forall a b. (a -> b) -> a -> b
$ \case IId -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x