decidable 0.1.5.0 → 0.2.0.0

raw patch · 9 files changed

+290/−753 lines, 9 filesdep +functor-productsdep +microlensdep +vinyldep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependencies added: functor-products, microlens, vinyl

Dependency ranges changed: singletons

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• decidable.cabal +8/−5
• src/Data/Type/Predicate.hs +95/−2
• src/Data/Type/Predicate/Auto.hs +20/−28
• src/Data/Type/Predicate/Logic.hs +1/−1
• src/Data/Type/Predicate/Param.hs +1/−0
• src/Data/Type/Predicate/Quantification.hs +10/−11
• src/Data/Type/Universe.hs +140/−702
• src/Data/Type/Universe/Subset.hs +5/−4

@@ -1,6 +1,16 @@ Changelog ========= +Version 0.2.0.0+---------------++*August 12, 2019*++<https://github.com/mstksg/decidable/releases/tag/v0.2.0.0>++*   Full restructuring of the Universe system, pulling it all out into a new+    package, *functor-products*.+ Version 0.1.5.0 --------------- 

@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.0.+-- This file has been generated from package.yaml by hpack version 0.31.2. -- -- see: https://github.com/sol/hpack ----- hash: 39c525768bc5e732a9d0d8a6b1931c269a0e4339a68d83434f6b3a4cf3f80c9f+-- hash: 91c5808428e945b6349291657cb7510e476dba940bd88509714b4178da856af3  name:           decidable-version:        0.1.5.0+version:        0.2.0.0 synopsis:       Combinators for manipulating dependently-typed predicates. description:    This library provides combinators and typeclasses for working and manipulating                 type-level predicates in Haskell, which are represented as matchable type-level@@ -22,7 +22,7 @@ copyright:      (c) Justin Le 2018 license:        BSD3 license-file:   LICENSE-tested-with:    GHC >= 8.4 && < 8.8+tested-with:    GHC >= 8.6 build-type:     Simple extra-source-files:     README.md@@ -48,5 +48,8 @@   ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns   build-depends:       base >=4.11 && <5-    , singletons >=2.4+    , functor-products+    , microlens+    , singletons >=2.5+    , vinyl   default-language: Haskell2010

@@ -1,8 +1,10 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds     #-} {-# LANGUAGE DefaultSignatures   #-}+{-# LANGUAGE EmptyCase           #-} {-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE FlexibleInstances   #-}+{-# LANGUAGE InstanceSigs        #-} {-# LANGUAGE LambdaCase          #-} {-# LANGUAGE RankNTypes          #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -27,7 +29,7 @@     -- * Predicates     Predicate, Wit(..)     -- ** Construct Predicates-  , TyPred, Evident, EqualTo, BoolPred, Impossible+  , TyPred, Evident, EqualTo, BoolPred, Impossible, In     -- ** Manipulate predicates   , PMap, type Not, decideNot     -- * Provable Predicates@@ -50,12 +52,17 @@   , mapRefuted   ) where +import           Data.Functor.Identity import           Data.Kind+import           Data.List.NonEmpty                    (NonEmpty(..)) import           Data.Maybe import           Data.Singletons import           Data.Singletons.Decide-import           Data.Singletons.Prelude hiding (Not)+import           Data.Singletons.Prelude hiding        (Not, ElemSym1)+import           Data.Singletons.Prelude.Identity+import           Data.Type.Functor.Product import           Data.Void+import qualified Data.Singletons.Prelude.List.NonEmpty as NE  -- | A type-level predicate in Haskell.  We say that the predicate @P :: -- 'Predicate' k@ is true/satisfied by input @x :: k@ if there exists@@ -354,6 +361,37 @@ instance Provable Evident where     prove = id +-- | @since 2.0.0+instance Provable (TyPred (Rec Sing)) where+    prove = singProd+-- | @since 2.0.0+instance Decidable (TyPred (Rec Sing))+-- | @since 2.0.0+instance Provable (TyPred (PMaybe Sing)) where+    prove = singProd+-- | @since 2.0.0+instance Decidable (TyPred (PMaybe Sing))+-- | @since 2.0.0+instance Provable (TyPred (NERec Sing)) where+    prove = singProd+-- | @since 2.0.0+instance Decidable (TyPred (NERec Sing))+-- | @since 2.0.0+instance Provable (TyPred (PIdentity Sing)) where+    prove = singProd+-- | @since 2.0.0+instance Decidable (TyPred (PIdentity Sing))+-- | @since 2.0.0+instance Provable (TyPred (PEither Sing)) where+    prove = singProd+-- | @since 2.0.0+instance Decidable (TyPred (PEither Sing))+-- | @since 2.0.0+instance Provable (TyPred (PTup Sing)) where+    prove = singProd+-- | @since 2.0.0+instance Decidable (TyPred (PTup Sing))+ instance (Decidable p, SingI f) => Decidable (PMap f p) where     decide = decide @p . applySing (sing :: Sing f) @@ -463,3 +501,58 @@     -> Refuted b     -> Refuted a mapRefuted = flip (.)++-- | @'In' f as@ is a predicate that a given input @a@ is a member of+-- collection @as@.+type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as++instance (SDecide k, SingI (as :: [k])) => Decidable (In [] as) where+    decide :: forall a. Sing a -> Decision (Index as a)+    decide x = go (sing @as)+      where+        go :: Sing bs -> Decision (Index bs a)+        go = \case+          SNil         -> Disproved $ \case {}+          y `SCons` ys -> case x %~ y of+            Proved Refl -> Proved IZ+            Disproved v -> case go ys of+              Proved i    -> Proved (IS i)+              Disproved u -> Disproved $ \case+                IZ   -> v Refl+                IS i -> u i++instance (SDecide k, SingI (as :: Maybe k)) => Decidable (In Maybe as) where+    decide x = case sing @as of+      SNothing -> Disproved $ \case {}+      SJust y  -> case x %~ y of+        Proved Refl -> Proved IJust+        Disproved v -> Disproved $ \case IJust -> v Refl++instance (SDecide k, SingI (as :: Either j k)) => Decidable (In (Either j) as) where+    decide x = case sing @as of+      SLeft _  -> Disproved $ \case {}+      SRight y -> case x %~ y of+        Proved Refl -> Proved IRight+        Disproved v -> Disproved $ \case IRight -> v Refl++instance (SDecide k, SingI (as :: NonEmpty k)) => Decidable (In NonEmpty as) where+    decide x = case sing @as of+      y NE.:%| (Sing :: Sing bs) -> case x %~ y of+        Proved Refl -> Proved NEHead+        Disproved v -> case decide @(In [] bs) x of+          Proved i    -> Proved $ NETail i+          Disproved u -> Disproved $ \case+            NEHead   -> v Refl+            NETail i -> u i++instance (SDecide k, SingI (as :: (j, k))) => Decidable (In ((,) j) as) where+    decide x = case sing @as of+      STuple2 _ y -> case x %~ y of+        Proved Refl -> Proved ISnd+        Disproved v -> Disproved $ \case ISnd -> v Refl++instance (SDecide k, SingI (as :: Identity k)) => Decidable (In Identity as) where+    decide x = case sing @as of+      SIdentity y -> case x %~ y of+        Proved Refl -> Proved IId+        Disproved v -> Disproved $ \case IId -> v Refl

@@ -43,6 +43,7 @@ import           Data.Singletons import           Data.Singletons.Sigma import           Data.Type.Equality+import           Data.Type.Functor.Product import           Data.Type.Predicate import           Data.Type.Predicate.Logic import           Data.Type.Predicate.Param@@ -167,18 +168,9 @@ instance AutoElem ((,) j) '(w, a) a where     autoElem = ISnd --- TODO: ???--- instance AutoElem (f :.: g) p ('Comp ass) where- instance AutoElem Identity ('Identity a) a where     autoElem = IId -instance AutoElem f as a => AutoElem (f :+: g) ('InL as) a where-    autoElem = IInL autoElem--instance AutoElem g bs b => AutoElem (f :+: g) ('InR bs) b where-    autoElem = IInR autoElem- instance AutoElem f as a => Auto (In f as) a where     auto = autoElem @f @as @a @@ -219,25 +211,12 @@         NEHead   -> auto @_ @p @a         NETail i -> runWitAll (autoAll @[] @p @as) i -instance AutoAll f (All g p) ass => AutoAll (f :.: g) p ('Comp ass) where-    autoAll = WitAll $ \(i :? j) ->-      runWitAll (runWitAll (autoAll @f @(All g p) @ass) i) j- instance Auto p a => AutoAll ((,) j) p '(w, a) where     autoAll = WitAll $ \case ISnd -> auto @_ @p @a -instance AutoAll Proxy p 'Proxy where-    autoAll = WitAll $ \case {}- instance Auto p a => AutoAll Identity p ('Identity a) where     autoAll = WitAll $ \case IId -> auto @_ @p @a -instance AutoAll f p as => AutoAll (f :+: g) p ('InL as) where-    autoAll = allSumL $ autoAll @f @p @as--instance AutoAll g p bs => AutoAll (f :+: g) p ('InR bs) where-    autoAll = allSumR $ autoAll @g @p @bs- -- | @since 0.1.2.0 instance AutoAll f p as => Auto (All f p) as where     auto = autoAll @f @p @as@@ -265,12 +244,6 @@ instance SingI a => Auto (NotNull Identity) ('Identity a) where     auto = WitAny IId sing -instance Auto (NotNull f) as => Auto (NotNull (f :+: g)) ('InL as) where-    auto = anySumL $ auto @_ @(NotNull f) @as--instance Auto (NotNull g) bs => Auto (NotNull (f :+: g)) ('InR bs) where-    auto = anySumR $ auto @_ @(NotNull g) @bs- -- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to -- not be true at compiletime. --@@ -339,3 +312,22 @@ instance (SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p))) as where     auto = mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p))          $ auto @_ @(Not (Any f (Found p))) @as++-- | @since 2.0.0+instance SingI as => Auto (TyPred (Rec Sing)) as where+    auto = singProd sing+-- | @since 2.0.0+instance SingI as => Auto (TyPred (PMaybe Sing)) as where+    auto = singProd sing+-- | @since 2.0.0+instance SingI as => Auto (TyPred (NERec Sing)) as where+    auto = singProd sing+-- | @since 2.0.0+instance SingI as => Auto (TyPred (PEither Sing)) as where+    auto = singProd sing+-- | @since 2.0.0+instance SingI as => Auto (TyPred (PTup Sing)) as where+    auto = singProd sing+-- | @since 2.0.0+instance SingI as => Auto (TyPred (PIdentity Sing)) as where+    auto = singProd sing

@@ -208,7 +208,7 @@  -- | We cannot have both @p@ and @'Not' p@. ----- (Renamed in v0.1.4.0; used to be 'excludedMiddle')+-- (Renamed in v0.1.4.0; used to be @excludedMiddle@) -- -- @since 0.1.4.0 complementation :: forall p. (p &&& Not p) --> Impossible

@@ -44,6 +44,7 @@ import           Data.Singletons.Decide import           Data.Singletons.Prelude.Tuple import           Data.Singletons.Sigma+import           Data.Type.Functor.Product import           Data.Type.Predicate import           Data.Type.Predicate.Logic import           Data.Type.Universe

@@ -25,8 +25,6 @@   , decideAny, idecideAny, decideNone, idecideNone   -- ** Entailment   , entailAny, ientailAny, entailAnyF, ientailAnyF-  -- ** Composition-  , allComp, compAll   -- * All   , All, WitAll(..), NotAll   -- ** Decision@@ -34,8 +32,6 @@   -- ** Entailment   , entailAll, ientailAll, entailAllF, ientailAllF   , decideEntailAll, idecideEntailAll-  -- ** Composition-  , anyComp, compAny   -- * Logical interplay   , allToAny   , allNotNone, noneAllNot@@ -45,6 +41,7 @@ import           Data.Kind import           Data.Singletons import           Data.Singletons.Decide+import           Data.Type.Functor.Product import           Data.Type.Predicate import           Data.Type.Predicate.Logic import           Data.Type.Universe@@ -74,7 +71,7 @@     => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)        -- ^ implication     -> Any f p @@ as     -> Any f q @@ as-ientailAny f (WitAny i x) = WitAny i (f i (index i sing) x)+ientailAny f (WitAny i x) = WitAny i (f i (indexSing i sing) x)  -- | If there exists an @a@ s.t. @p a@, and if @p@ implies @q@, then there -- must exist an @a@ s.t. @q a@.@@ -90,7 +87,7 @@     => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)      -- ^ implication     -> All f p @@ as     -> All f q @@ as-ientailAll f a = WitAll $ \i -> f i (index i sing) (runWitAll a i)+ientailAll f a = WitAll $ \i -> f i (indexSing i sing) (runWitAll a i)  -- | If for all @a@ we have @p a@, and if @p@ implies @q@, then for all @a@ -- we must also have @p a@.@@ -124,7 +121,7 @@     => (p --># q) h                                     -- ^ implication in context     -> (Any f p --># Any f q) h entailAnyF f x a = withSingI x $-    ientailAnyF @f @p @q (\i -> f (index i x)) a+    ientailAnyF @f @p @q (\i -> f (indexSing i x)) a  -- | 'entailAllF', but providing an 'Elem'. ientailAllF@@ -132,7 +129,9 @@     => (forall a. Elem f as a -> p @@ a -> h (q @@ a))    -- ^ implication in context     -> All f p @@ as     -> h (All f q @@ as)-ientailAllF f a = igenAllA (\i _ -> f i (runWitAll a i)) sing+ientailAllF f a = fmap (prodAll getWit)+                . itraverseProd (\i _ -> Wit @q <$> f i (runWitAll a i))+                $ singProd (sing @as)  -- | If @p@ implies @q@ under some context @h@, and if we have @p a@ for -- all @a@, then we must have @q a@ for all @a@ under context @h@.@@ -141,7 +140,7 @@     => (p --># q) h                                     -- ^ implication in context     -> (All f p --># All f q) h entailAllF f x a = withSingI x $-    ientailAllF @f @p @q (\i -> f (index i x)) a+    ientailAllF @f @p @q (\i -> f (indexSing i x)) a  -- | 'entailAllF', but providing an 'Elem'. idecideEntailAll@@ -163,7 +162,7 @@ -- -- @since 0.1.2.0 anyImpossible :: Universe f => Any f Impossible --> Impossible-anyImpossible _ (WitAny i p) = p . index i+anyImpossible _ (WitAny i p) = p . indexSing i  -- | If any @a@ in @as@ does not satisfy @p@, then not all @a@ in @as@ -- satisfy @p@.@@ -182,7 +181,7 @@     => NotAll f p --> Any f (Not p) notAllAnyNot xs vAll = elimDisproof (decide @(Any f (Not p)) xs) $ \vAny ->     vAll $ WitAll $ \i ->-      elimDisproof (decide @p (index i xs)) $ \vP ->+      elimDisproof (decide @p (indexSing i xs)) $ \vP ->         vAny $ WitAny i vP  -- | If @p@ is false for all @a@ in @as@, then no @a@ in @as@ satisfies

@@ -1,21 +1,21 @@-{-# 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 TypeFamilies        #-}-{-# LANGUAGE TypeInType          #-}-{-# LANGUAGE TypeOperators       #-}+{-# 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@@ -32,9 +32,9 @@ module Data.Type.Universe (   -- * Universe     Elem, In, Universe(..)+  , singAll   -- ** Instances-  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IProxy, IIdentity(..)-  , CompElem(..), SumElem(..)+  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IIdentity(..)   -- ** Predicates   , All, WitAll(..), NotAll   , Any, WitAny(..), None@@ -42,59 +42,26 @@   -- *** Specialized   , IsJust, IsNothing, IsRight, IsLeft   -- * Decisions and manipulations-  , decideAny, decideAll, genAllA, genAll, igenAll-  , foldMapUni, ifoldMapUni, index, pickElem-  -- * Universe Combination-  -- ** Universe Composition-  , (:.:)(..), sGetComp, GetComp-  , allComp, compAll, anyComp, compAny-  -- ** Universe Disjunction-  , (:+:)(..)-  , anySumL, anySumR, sumLAny, sumRAny-  , allSumL, allSumR, sumLAll, sumRAll-  -- * Defunctionalization symbols-  , ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1-  -- * Singletons-  , SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIProxy, SIIdentity(..)-  , Sing (SComp, SInL, SIndex', SIJust', SIRight', SNEIndex', SISnd', SIProxy', SIIdentity')+  , decideAny, decideAll+  , genAll, igenAll+  , splitSing+  , pickElem   ) where -import           Control.Applicative import           Data.Functor.Identity import           Data.Kind import           Data.List.NonEmpty                    (NonEmpty(..))-import           Data.Proxy 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           Data.Typeable                         (Typeable)-import           GHC.Generics                          (Generic)+import           GHC.Generics                          ((:*:)(..)) import           Prelude hiding                        (any, all) import qualified Data.Singletons.Prelude.List.NonEmpty as NE -#if MIN_VERSION_singletons(2,5,0)-import           Data.Singletons.Prelude.Identity-#else-import           Data.Singletons.TH-genSingletons [''Identity]-#endif---- | A witness for membership of a given item in a type-level collection-type family Elem (f :: Type -> Type) :: f k -> k -> Type--data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type-data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type-type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a--type instance Apply (ElemSym0 f) as = ElemSym1 f as-type instance Apply (ElemSym1 f as) a = Elem f as a---- | @'In' f as@ is a predicate that a given input @a@ is a member of--- collection @as@.-type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as- -- | 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@@ -135,20 +102,21 @@     prove _ (WitAny i s) = WitAny i (prove @p s)  instance (Universe f, Provable p) => Provable (All f p) where-    prove xs = WitAll $ \i -> prove @p (index i xs)+    prove xs = WitAll $ \i -> prove @p (indexSing i xs)  instance Universe f => TFunctor (Any f) where-    tmap f xs (WitAny i x) = WitAny i (f (index i xs) x)+    tmap f xs (WitAny i x) = WitAny i (f (indexSing i xs) x)  instance Universe f => TFunctor (All f) where-    tmap f xs a = WitAll $ \i -> f (index i xs) (runWitAll a i)+    tmap f xs a = WitAll $ \i -> f (indexSing i xs) (runWitAll a i)  instance Universe f => DFunctor (All f) where     dmap f xs a = idecideAll (\i x -> f x (runWitAll a i)) xs  -- | Typeclass for a type-level container that you can quantify or lift -- type-level predicates over.-class Universe (f :: Type -> Type) where+class FProd f => Universe (f :: Type -> Type) where+     -- | 'decideAny', but providing an 'Elem'.     idecideAny         :: forall k (p :: k ~> Type) (as :: f k). ()@@ -161,12 +129,17 @@         => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value         -> (Sing as -> Decision (All f p @@ as))                         -- ^ predicate on collection -    -- | 'genAllA', but providing an 'Elem'.-    igenAllA-        :: forall k (p :: k ~> Type) (as :: f k) h. Applicative h-        => (forall a. Elem f as a -> Sing a -> h (p @@ a))        -- ^ predicate on value in context-        -> (Sing as -> h (All f p @@ as))                              -- ^ predicate on collection in context+    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)) @@ -210,28 +183,28 @@     -> Decide (All f p)                -- ^ predicate on collection decideAll f = idecideAll (const f) --- | If @p a@ is true for all values @a@ in @as@ under some--- (Applicative) context @h@, then you can create an @'All' p as@ under--- that Applicative context @h@.------ Can be useful with 'Identity' (which is basically unwrapping and--- wrapping 'All'), or with 'Maybe' (which can express predicates that--- are either provably true or not provably false).------ In practice, this can be used to iterate and traverse and sequence--- actions over all "items" in @as@.-genAllA-    :: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h)-    => (forall a. Sing a -> h (p @@ a))        -- ^ predicate on value in context-    -> (Sing as -> h (All f p @@ as))               -- ^ predicate on collection in context-genAllA f = igenAllA (const 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 = prodAll id . 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 = mapDecision (\case WitAny i Refl -> i)+                       (\case i -> WitAny i Refl)+         . decide @(Any f (TyPred ((:~:) a)))+         $ sing+ -- | 'genAll', but providing an 'Elem'. igenAll     :: forall f k (p :: k ~> Type) (as :: f k). Universe f     => (forall a. Elem f as a -> Sing a -> p @@ a)            -- ^ always-true predicate on value     -> (Sing as -> All f p @@ as)                                  -- ^ always-true predicate on collection-igenAll f = runIdentity . igenAllA (\i -> Identity . f i)+igenAll f = prodAll (\(i :*: x) -> f i x) . imapProd (:*:) . singProd  -- | If @p a@ is true for all values @a@ in @as@, then we have @'All' -- p as@.  Basically witnesses the definition of 'All'.@@ -239,110 +212,36 @@     :: forall f k (p :: k ~> Type). Universe f     => Prove p                 -- ^ always-true predicate on value     -> Prove (All f p)         -- ^ always-true predicate on collection-genAll f = igenAll (const f)---- | Extract the item from the container witnessed by the 'Elem'-index-    :: forall f as a. Universe f-    => Elem f as a        -- ^ Witness-    -> Sing as            -- ^ Collection-    -> Sing a-index i = (`runWitAll` i) . splitSing+genAll f = prodAll f . singProd  -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.-splitSing+singAll     :: forall f k (as :: f k). Universe f     => Sing as-    -> All f (TyPred Sing) @@ as-splitSing = igenAll @f @_ @(TyPred Sing) (\_ x -> x)---- | 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 = mapDecision (\case WitAny i Refl -> i)-                       (\case i -> WitAny i Refl)-         . decide @(Any f (TyPred ((:~:) a)))-         $ sing---- | 'foldMapUni' but with access to the index.-ifoldMapUni-    :: forall f k (as :: f k) m. (Universe f, Monoid m)-    => (forall a. Elem f as a -> Sing a -> m)-    -> Sing as-    -> m-ifoldMapUni f = getConst . igenAllA (\i -> Const . f i)---- | A 'foldMap' over all items in a collection.-foldMapUni-    :: forall f k (as :: f k) m. (Universe f, Monoid m)-    => (forall (a :: k). Sing a -> m)-    -> Sing as-    -> m-foldMapUni f = ifoldMapUni (const f)+    -> All f Evident @@ as+singAll = prodAll id . singProd --- | Witness an item in a type-level list by providing its index.-data Index :: [k] -> k -> Type where-    IZ :: Index (a ': as) a-    IS :: Index bs a -> Index (b ': bs) a+-- | Test that a 'Maybe' is 'Just'.+--+-- @since 0.1.2.0+type IsJust    = (NotNull Maybe :: Predicate (Maybe k)) -deriving instance Show (Index as a)-instance (SingI (as :: [k]), SDecide k) => Decidable (TyPred (Index as)) where-    decide x = withSingI x $ pickElem+-- | Test that a 'Maybe' is 'Nothing'.+--+-- @since 0.1.2.0+type IsNothing = (Null    Maybe :: Predicate (Maybe k)) -type instance Elem [] = Index+-- | Test that an 'Either' is 'Right'+--+-- @since 0.1.2.0+type IsRight = (NotNull (Either j) :: Predicate (Either j k)) --- | Kind-indexed singleton for 'Index'.  Provided as a separate data--- declaration to allow you to use these at the type level.  However, the--- main interface is still provided through the newtype wrapper 'SIndex'',--- which has an actual proper 'Sing' instance.+-- | Test that an 'Either' is 'Left' ----- @since 0.1.5.0-data SIndex as a :: Index as a -> Type where-    SIZ :: SIndex (a ': as) a 'IZ-    SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i)+-- @since 0.1.2.0+type IsLeft  = (Null    (Either j) :: Predicate (Either j k)) -deriving instance Show (SIndex as a i) -newtype instance Sing (i :: Index as a) where-    SIndex' :: SIndex as a i -> Sing i--instance SingI 'IZ where-    sing = SIndex' SIZ--instance SingI i => SingI ('IS i) where-    sing = case sing of-      SIndex' i -> SIndex' (SIS i)--instance SingKind (Index as a) where-    type Demote (Index as a) = Index as a-    fromSing (SIndex' i) = go i-      where-        go :: SIndex bs b i -> Index bs b-        go = \case-          SIZ   -> IZ-          SIS j -> IS (go j)-    toSing i = go i (SomeSing . SIndex')-      where-        go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r-        go = \case-          IZ   -> ($ SIZ)-          IS j -> \f -> go j (f . SIS)--instance SDecide (Index as a) where-    SIndex' i %~ SIndex' j = go i j-      where-        go :: SIndex bs b i -> SIndex bs b j -> Decision (i :~: j)-        go = \case-          SIZ -> \case-            SIZ   -> Proved Refl-            SIS _ -> Disproved $ \case {}-          SIS i' -> \case-            SIZ   -> Disproved $ \case {}-            SIS j' -> case go i' j' of-              Proved Refl -> Proved Refl-              Disproved v -> Disproved $ \case Refl -> v Refl- instance Universe [] where     idecideAny         :: forall k (p :: k ~> Type) (as :: [k]). ()@@ -375,65 +274,31 @@           Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)         Disproved v -> Disproved $ \a -> v $ runWitAll a IZ -    igenAllA-        :: forall k (p :: k ~> Type) (as :: [k]) h. Applicative h-        => (forall a. Elem [] as a -> Sing a -> h (p @@ a))-        -> Sing as-        -> h (All [] p @@ as)-    igenAllA f = \case-        SNil         -> pure $ WitAll $ \case {}-        x `SCons` xs -> go <$> f IZ x <*> igenAllA (f . IS) xs+    allProd+        :: forall p g. ()+        => (forall a. Sing a -> p @@ a -> g a)+        -> All [] p --> TyPred (Prod [] g)+    allProd f = go       where-        go :: p @@ b -> All [] p @@ bs -> All [] p @@ (b ': bs)-        go p a = WitAll $ \case-          IZ   -> p-          IS i -> runWitAll a i---- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is--- 'Just'.-data IJust :: Maybe k -> k -> Type where-    IJust :: IJust ('Just a) a--deriving instance Show (IJust as a)-instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IJust as)) where-    decide x = withSingI x $ pickElem---- | Kind-indexed singleton for 'IJust'.  Provided as a separate data--- declaration to allow you to use these at the type level.  However, the--- main interface is still provided through the newtype wrapper 'SIJust'',--- which has an actual proper 'Sing' instance.------ @since 0.1.5.0-data SIJust as a :: IJust as a -> Type where-    SIJust :: SIJust ('Just a) a 'IJust--deriving instance Show (SIJust as a i)--newtype instance Sing (i :: IJust as a) where-    SIJust' :: SIJust as a i -> Sing i--instance SingI 'IJust where-    sing = SIJust' SIJust--instance SingKind (IJust as a) where-    type Demote (IJust as a) = IJust as a-    fromSing (SIJust' SIJust) = IJust-    toSing IJust = SomeSing (SIJust' SIJust)--instance SDecide (IJust as a) where-    SIJust' SIJust %~ SIJust' SIJust = Proved Refl--type instance Elem Maybe = IJust---- | Test that a 'Maybe' is 'Just'.------ @since 0.1.2.0-type IsJust    = (NotNull Maybe :: Predicate (Maybe k))+        go :: Sing as -> WitAll [] p as -> Prod [] g as+        go = \case+          SNil         -> \_ -> RNil+          x `SCons` xs -> \a -> f x (runWitAll a IZ)+                             :& go xs (WitAll (runWitAll a . IS)) --- | Test that a 'Maybe' is 'Nothing'.------ @since 0.1.2.0-type IsNothing = (Null    Maybe :: Predicate (Maybe k))+    prodAll+        :: forall p g as. ()+        => (forall a. g a -> p @@ a)+        -> Prod [] g as+        -> All [] p @@ as+    prodAll f = go+      where+        go :: Prod [] g bs -> All [] p @@ bs+        go = \case+          RNil    -> WitAll $ \case {}+          x :& xs -> WitAll $ \case+            IZ   -> f x+            IS i -> runWitAll (go xs) i  instance Universe Maybe where     idecideAny f = \case@@ -442,62 +307,17 @@         Proved p    -> Proved $ WitAny IJust p         Disproved v -> Disproved $ \case           WitAny IJust p -> v p-     idecideAll f = \case       SNothing -> Proved $ WitAll $ \case {}       SJust x  -> case f IJust x of         Proved p    -> Proved $ WitAll $ \case IJust -> p         Disproved v -> Disproved $ \a -> v $ runWitAll a IJust--    igenAllA f = \case-      SNothing -> pure $ WitAll $ \case {}-      SJust x  -> (\p -> WitAll $ \case IJust -> p) <$> f IJust x---- | Witness an item in a type-level @'Either' j@ by proving the 'Either'--- is 'Right'.-data IRight :: Either j k -> k -> Type where-    IRight :: IRight ('Right a) a--deriving instance Show (IRight as a)-instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IRight as)) where-    decide x = withSingI x $ pickElem---- | Kind-indexed singleton for 'IRight'.  Provided as a separate data--- declaration to allow you to use these at the type level.  However, the--- main interface is still provided through the newtype wrapper 'SIRight'',--- which has an actual proper 'Sing' instance.------ @since 0.1.5.0-data SIRight as a :: IRight as a -> Type where-    SIRight :: SIRight ('Right a) a 'IRight--deriving instance Show (SIRight as a i)--newtype instance Sing (i :: IRight as a) where-    SIRight' :: SIRight as a i -> Sing i--instance SingI 'IRight where-    sing = SIRight' SIRight--instance SingKind (IRight as a) where-    type Demote (IRight as a) = IRight as a-    fromSing (SIRight' SIRight) = IRight-    toSing IRight = SomeSing (SIRight' SIRight)--instance SDecide (IRight as a) where-    SIRight' SIRight %~ SIRight' SIRight = Proved Refl--type instance Elem (Either j) = IRight---- | 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))+    allProd f = \case+      SNothing -> \_ -> PNothing+      SJust x  -> \a -> PJust (f x (runWitAll a IJust))+    prodAll f = \case+      PNothing -> WitAll $ \case {}+      PJust x  -> WitAll $ \case IJust -> f x  instance Universe (Either j) where     idecideAny f = \case@@ -506,71 +326,17 @@         Proved p    -> Proved $ WitAny IRight p         Disproved v -> Disproved $ \case           WitAny IRight p -> v p-     idecideAll f = \case       SLeft  _ -> Proved $ WitAll $ \case {}       SRight x -> case f IRight x of         Proved p    -> Proved $ WitAll $ \case IRight -> p         Disproved v -> Disproved $ \a -> v $ runWitAll a IRight--    igenAllA f = \case-      SLeft  _ -> pure $ WitAll $ \case {}-      SRight x -> (\p -> WitAll $ \case IRight -> p) <$> f IRight x---- | Witness an item in a type-level 'NonEmpty' by either indicating that--- it is the "head", or by providing an index in the "tail".-data NEIndex :: NonEmpty k -> k -> Type where-    NEHead :: NEIndex (a ':| as) a-    NETail :: Index as a -> NEIndex (b ':| as) a--deriving instance Show (NEIndex as a)-instance (SingI (as :: NonEmpty k), SDecide k) => Decidable (TyPred (NEIndex as)) where-    decide x = withSingI x $ pickElem---- | Kind-indexed singleton for 'NEIndex'.  Provided as a separate data--- declaration to allow you to use these at the type level.  However, the--- main interface is still provided through the newtype wrapper--- 'SNEIndex'', which has an actual proper 'Sing' instance.------ @since 0.1.5.0-data SNEIndex as a :: NEIndex as a -> Type where-    SNEHead :: SNEIndex (a ':| as) a 'NEHead-    SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)--deriving instance Show (SNEIndex as a i)--newtype instance Sing (i :: NEIndex as a) where-    SNEIndex' :: SNEIndex as a i -> Sing i--instance SingI 'NEHead where-    sing = SNEIndex' SNEHead--instance SingI i => SingI ('NETail i) where-    sing = case sing of-      SIndex' i -> SNEIndex' (SNETail i)--instance SingKind (NEIndex as a) where-    type Demote (NEIndex as a) = NEIndex as a-    fromSing = \case-      SNEIndex' SNEHead     -> NEHead-      SNEIndex' (SNETail i) -> NETail $ fromSing (SIndex' i)-    toSing = \case-      NEHead   -> SomeSing (SNEIndex' SNEHead)-      NETail i -> withSomeSing i $ \case-        SIndex' j -> SomeSing (SNEIndex' (SNETail j))--instance SDecide (NEIndex as a) where-    (%~) = \case-      SNEIndex' SNEHead -> \case-        SNEIndex' SNEHead     -> Proved Refl-        SNEIndex' (SNETail _) -> Disproved $ \case {}-      SNEIndex' (SNETail i) -> \case-        SNEIndex' SNEHead -> Disproved $ \case {}-        SNEIndex' (SNETail j) -> case SIndex' i %~ SIndex' j of-          Proved Refl -> Proved Refl-          Disproved v -> Disproved $ \case Refl -> v Refl--type instance Elem NonEmpty = NEIndex+    allProd f = \case+      SLeft  w -> \_ -> PLeft w+      SRight x -> \a -> PRight (f x (runWitAll a IRight))+    prodAll f = \case+      PLeft _  -> WitAll $ \case {}+      PRight x -> WitAll $ \case IRight -> f x  instance Universe NonEmpty where     idecideAny@@ -600,369 +366,41 @@         Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)       Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead -    igenAllA-        :: forall k (p :: k ~> Type) (as :: NonEmpty k) h. Applicative h-        => (forall a. Elem NonEmpty as a -> Sing a -> h (p @@ a))-        -> Sing as-        -> h (All NonEmpty p @@ as)-    igenAllA f (x NE.:%| xs) = go <$> f NEHead x <*> igenAllA @[] @_ @p (f . NETail) xs-      where-        go :: p @@ b -> All [] p @@ bs -> All NonEmpty p @@ (b ':| bs)-        go p ps = WitAll $ \case-          NEHead   -> p-          NETail i -> runWitAll ps i---- | Trivially witness an item in the second field of a type-level tuple.-data ISnd :: (j, k) -> k -> Type where-    ISnd :: ISnd '(a, b) b--deriving instance Show (ISnd as a)--- TODO: does this interfere with NonNull stuff?-instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (ISnd as)) where-    decide x = withSingI x $ pickElem---- | Kind-indexed singleton for 'ISnd'.  Provided as a separate data--- declaration to allow you to use these at the type level.  However, the--- main interface is still provided through the newtype wrapper 'SISnd'',--- which has an actual proper 'Sing' instance.------ @since 0.1.5.0-data SISnd as a :: ISnd as a -> Type where-    SISnd :: SISnd '(a, b) b 'ISnd--deriving instance Show (SISnd as a i)--newtype instance Sing (i :: ISnd as a) where-    SISnd' :: SISnd as a i -> Sing i--instance SingI 'ISnd where-    sing = SISnd' SISnd--instance SingKind (ISnd as a) where-    type Demote (ISnd as a) = ISnd as a-    fromSing (SISnd' SISnd) = ISnd-    toSing ISnd = SomeSing (SISnd' SISnd)--instance SDecide (ISnd as a) where-    SISnd' SISnd %~ SISnd' SISnd = Proved Refl--type instance Elem ((,) j) = ISnd+    allProd+        :: forall p g. ()+        => (forall a. Sing a -> p @@ a -> g a)+        -> All NonEmpty p --> TyPred (Prod NonEmpty g)+    allProd f (x NE.:%| xs) a =+          f x (runWitAll a NEHead)+      :&| allProd @[] @p f xs (WitAll (runWitAll a . NETail))+    prodAll+        :: forall p g as. ()+        => (forall a. g a -> p @@ a)+        -> Prod NonEmpty g as+        -> All NonEmpty p @@ as+    prodAll f (x :&| xs) = WitAll $ \case+        NEHead   -> f x+        NETail i -> runWitAll (prodAll @[] @p f xs) i  instance Universe ((,) j) where     idecideAny f (STuple2 _ x) = case f ISnd x of       Proved p    -> Proved $ WitAny ISnd p       Disproved v -> Disproved $ \case WitAny ISnd p -> v p-     idecideAll f (STuple2 _ x) = case f ISnd x of       Proved p    -> Proved $ WitAll $ \case ISnd -> p       Disproved v -> Disproved $ \a -> v $ runWitAll a ISnd--    igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case ISnd -> p) <$> f ISnd x---- | There are no items of type @a@ in a @'Proxy' a@.------ @since 0.1.3.0-data IProxy :: Proxy k -> k -> Type--deriving instance Show (IProxy 'Proxy a)--instance Provable (Not (TyPred (IProxy 'Proxy))) where-    prove _ = \case {}---- | Kind-indexed singleton for 'IProxy'.  Provided as a separate data--- declaration to allow you to use these at the type level.  However, the--- main interface is still provided through the newtype wrapper 'SIProxy'',--- which has an actual proper 'Sing' instance.------ @since 0.1.5.0-data SIProxy as a :: IProxy as a -> Type--deriving instance Show (SIProxy as a i)--newtype instance Sing (i :: IProxy as a) where-    SIProxy' :: SIProxy as a i -> Sing i--instance SingKind (IProxy as a) where-    type Demote (IProxy as a) = IProxy as a-    fromSing (SIProxy' i) = case i of {}-    toSing = \case {}--instance SDecide (IProxy as a) where-    SIProxy' i %~ SIProxy' _ = Proved $ case i of {}--type instance Elem Proxy = IProxy---- | The null universe-instance Universe Proxy where-    idecideAny _ _ = Disproved $ \case-        WitAny i _ -> case i of {}-    idecideAll _ _ = Proved $ WitAll $ \case {}-    igenAllA   _ _ = pure $ WitAll $ \case {}---- | Trivially witness the item held in an 'Identity'.------ @since 0.1.3.0-data IIdentity :: Identity k -> k -> Type where-    IId :: IIdentity ('Identity x) x--deriving instance Show (IIdentity as a)--instance (SingI (as :: Identity k), SDecide k) => Decidable (TyPred (IIdentity as)) where-    decide x = withSingI x $ pickElem---- | Kind-indexed singleton for 'IIdentity'.  Provided as a separate data--- declaration to allow you to use these at the type level.  However, the--- main interface is still provided through the newtype wrapper 'SIIdentity'',--- which has an actual proper 'Sing' instance.------ @since 0.1.5.0-data SIIdentity as a :: IIdentity as a -> Type where-    SIId :: SIIdentity ('Identity a) a 'IId--deriving instance Show (SIIdentity as a i)--newtype instance Sing (i :: IIdentity as a) where-    SIIdentity' :: SIIdentity as a i -> Sing i--instance SingI 'IId where-    sing = SIIdentity' SIId--instance SingKind (IIdentity as a) where-    type Demote (IIdentity as a) = IIdentity as a-    fromSing (SIIdentity' SIId) = IId-    toSing IId = SomeSing (SIIdentity' SIId)--instance SDecide (IIdentity as a) where-    SIIdentity' SIId %~ SIIdentity' SIId = Proved Refl--type instance Elem Identity = IIdentity+    allProd f (STuple2 w x) a = PTup w $ f x (runWitAll a ISnd)+    prodAll f (PTup _ x) = WitAll $ \case ISnd -> f x --- | The single-pointed universe.  Note that this instance is really only--- usable in /singletons-2.5/ and higher (so GHC 8.6).+-- | The single-pointed universe. instance Universe Identity where-    idecideAny f (SIdentity x) = mapDecision (WitAny IId)-                                             (\case WitAny IId p -> p)-                               $ f IId x-    idecideAll f (SIdentity x) = mapDecision (\p -> WitAll $ \case IId -> p)-                                             (`runWitAll` IId)-                               $ f IId x-    igenAllA f (SIdentity x) = (\p -> WitAll $ \case IId -> p) <$> f IId x---- | Compose two Functors.  Is the same as 'Data.Functor.Compose.Compose'--- and 'GHC.Generics.:.:', except with a singleton and meant to be used at--- the type level.  Will be redundant if either of the above gets brought--- into the singletons library.------ Note that because this is a higher-kinded data constructor, there is no--- 'SingKind'  instance; if you need 'fromSing' and 'toSing', try going--- through 'Comp' and 'getComp' and 'SComp' and 'sGetComp'.------ Note that 'Identity' acts as an identity.------ @since 0.1.2.0-data (f :.: g) a = Comp { getComp :: f (g a) }-    deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)-deriving instance (Traversable f, Traversable g) => Traversable (f :.: g)--data instance Sing (k :: (f :.: g) a) where-    SComp :: Sing x -> Sing ('Comp x)---- | 'getComp' lifted to the type level------ @since 0.1.2.0-type family GetComp c where-    GetComp ('Comp a) = a---- | Singletonized witness for 'GetComp'------ @since 0.1.2.0-sGetComp :: Sing a -> Sing (GetComp a)-sGetComp (SComp x) = x--instance SingI ass => SingI ('Comp ass) where-    sing = SComp sing--data GetCompSym0 :: (f :.: g) k ~> f (g k)-type instance Apply GetCompSym0 ('Comp ass) = ass-type GetCompSym1 a = GetComp a---- instance forall f g a f' g' a'. (SingKind (f (g a)), Demote (f (g a)) ~ f' (g' a')) => SingKind ((f :.: g) a) where---     type Demote ((f :.: g) a) = (:.:) f' g' a'---- | A pair of indices allows you to index into a nested structure.------ @since 0.1.2.0-data CompElem :: (f :.: g) k -> k -> Type where-    (:?) :: Elem f ass as-         -> Elem g as  a-         -> CompElem ('Comp ass) a---- deriving instance ((forall as. Show (Elem f ass as)), (forall as. Show (Elem g as a)))---     => Show (CompElem ('Comp ass :: (f :.: g) k) a)--type instance Elem (f :.: g) = CompElem--instance (Universe f, Universe g) => Universe (f :.: g) where-    idecideAny-        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()-        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))-        -> Sing ass-        -> Decision (Any (f :.: g) p @@ ass)-    idecideAny f (SComp xss)-        = mapDecision anyComp compAny-        . idecideAny @f @_ @(Any g p) go-        $ xss-      where-        go  :: Elem f (GetComp ass) as-            -> Sing as-            -> Decision (Any g p @@ as)-        go i = idecideAny $ \j -> f (i :? j)--    idecideAll-        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()-        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))-        -> Sing ass-        -> Decision (All (f :.: g) p @@ ass)-    idecideAll f (SComp xss)-        = mapDecision allComp compAll-        . idecideAll @f @_ @(All g p) go-        $ xss-      where-        go  :: Elem f (GetComp ass) as-            -> Sing as-            -> Decision (All g p @@ as)-        go i = idecideAll $ \j -> f (i :? j)--    igenAllA-        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k) h. Applicative h-        => (forall a. Elem (f :.: g) ass a -> Sing a -> h (p @@ a))-        -> Sing ass-        -> h (All (f :.: g) p @@ ass)-    igenAllA f (SComp ass) = allComp <$> igenAllA @f @_ @(All g p) go ass-      where-        go  :: Elem f (GetComp ass) (as :: g k)-            -> Sing as-            -> h (All g p @@ as)-        go i = igenAllA $ \j -> f (i :? j)---- | Turn a composition of 'Any' into an 'Any' of a composition.------ @since 0.1.2.0-anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as-anyComp (WitAny i (WitAny j p)) = WitAny (i :? j) p---- | Turn an 'Any' of a composition into a composition of 'Any'.------ @since 0.1.2.0-compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as-compAny (WitAny (i :? j) p) = WitAny i (WitAny j p)---- | Turn a composition of 'All' into an 'All' of a composition.------ @since 0.1.2.0-allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as-allComp a = WitAll $ \(i :? j) -> runWitAll (runWitAll a i) j---- | Turn an 'All' of a composition into a composition of 'All'.------ @since 0.1.2.0-compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as-compAll a = WitAll $ \i -> WitAll $ \j -> runWitAll a (i :? j)---- | Disjoint union of two Functors.  Is the same as 'Data.Functor.Sum.Sum'--- and 'GHC.Generics.:+:', except with a singleton and meant to be used at--- the type level.  Will be redundant if either of the above gets brought--- into the singletons library.------ Note that because this is a higher-kinded data constructor, there is no--- 'SingKind'  instance; if you need 'fromSing' and 'toSing', consider--- manually pattern matching.------ Note that 'Proxy' acts as an identity.------ @since 0.1.3.0-data (f :+: g) a = InL (f a)-                 | InR (g a)-    deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)-deriving instance (Traversable f, Traversable g) => Traversable (f :+: g)--data instance Sing (k :: (f :+: g) a) where-    SInL :: Sing x -> Sing ('InL x)-    SInR :: Sing y -> Sing ('InR y)--type family FromL s where-    FromL ('InL a) = a---- | Index into a disjoint union by providing an index into one of the two--- possible options.------ @since 0.1.3.0-data SumElem :: (f :+: g) k -> k -> Type where-    IInL :: Elem f as a -> SumElem ('InL as) a-    IInR :: Elem f bs b -> SumElem ('InR bs) b--type instance Elem (f :+: g) = SumElem--instance (Universe f, Universe g) => Universe (f :+: g) where-    idecideAny-        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k). ()-        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> Decision (p @@ ab))-        -> Sing abs-        -> Decision (Any (f :+: g) p @@ abs)-    idecideAny f = \case-      SInL xs -> mapDecision anySumL sumLAny-               $ idecideAny @f @_ @p (f . IInL) xs-      SInR ys -> mapDecision anySumR sumRAny-               $ idecideAny @g @_ @p (f . IInR) ys--    idecideAll-        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k). ()-        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> Decision (p @@ ab))-        -> Sing abs-        -> Decision (All (f :+: g) p @@ abs)-    idecideAll f = \case-      SInL xs -> mapDecision allSumL sumLAll-               $ idecideAll @f @_ @p (f . IInL) xs-      SInR xs -> mapDecision allSumR sumRAll-               $ idecideAll @g @_ @p (f . IInR) xs--    igenAllA-        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k) h. Applicative h-        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> h (p @@ ab))-        -> Sing abs-        -> h (All (f :+: g) p @@ abs)-    igenAllA f = \case-      SInL xs -> allSumL <$> igenAllA @f @_ @p (f . IInL) xs-      SInR xs -> allSumR <$> igenAllA @g @_ @p (f . IInR) xs---- | Turn an 'Any' of @f@ into an 'Any' of @f ':+:' g@.-anySumL :: Any f p @@ as -> Any (f :+: g) p @@ 'InL as-anySumL (WitAny i x) = WitAny (IInL i) x---- | Turn an 'Any' of @g@ into an 'Any' of @f ':+:' g@.-anySumR :: Any g p @@ bs -> Any (f :+: g) p @@ 'InR bs-anySumR (WitAny j y) = WitAny (IInR j) y---- | Turn an 'Any' of @f ':+:' g@ into an 'Any' of @f@.-sumLAny :: Any (f :+: g) p @@ 'InL as -> Any f p @@ as-sumLAny (WitAny (IInL i) x) = WitAny i x---- | Turn an 'Any' of @f ':+:' g@ into an 'Any' of @g@.-sumRAny :: Any (f :+: g) p @@ 'InR bs -> Any g p @@ bs-sumRAny (WitAny (IInR j) y) = WitAny j y---- | Turn an 'All' of @f@ into an 'All' of @f ':+:' g@.-allSumL :: All f p @@ as -> All (f :+: g) p @@ 'InL as-allSumL a = WitAll $ \case IInL i -> runWitAll a i---- | Turn an 'All' of @g@ into an 'All' of @f ':+:' g@.-allSumR :: All g p @@ bs -> All (f :+: g) p @@ 'InR bs-allSumR a = WitAll $ \case IInR j -> runWitAll a j---- | Turn an 'All' of @f ':+:' g@ into an 'All' of @f@.-sumLAll :: All (f :+: g) p @@ 'InL as -> All f p @@ as-sumLAll a = WitAll $ runWitAll a . IInL---- | Turn an 'All' of @f ':+:' g@ into an 'All' of @g@.-sumRAll :: All (f :+: g) p @@ 'InR bs -> All g p @@ bs-sumRAll a = WitAll $ runWitAll a . IInR+    idecideAny f (SIdentity x) =+        mapDecision (WitAny IId)+                    (\case WitAny IId p -> p)+      $ f IId x+    idecideAll f (SIdentity x) =+        mapDecision (\p -> WitAll $ \case IId -> p)+                    (`runWitAll` IId)+      $ f IId x+    allProd f (SIdentity x) a = PIdentity $ f x (runWitAll a IId)+    prodAll f (PIdentity x) = WitAll $ \case IId -> f x

@@ -37,6 +37,7 @@ import           Data.Monoid                        (Alt(..)) import           Data.Singletons import           Data.Singletons.Decide+import           Data.Type.Functor.Product import           Data.Type.Predicate import           Data.Type.Predicate.Logic import           Data.Type.Predicate.Quantification@@ -63,7 +64,7 @@     => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))     -> Sing as     -> Subset f p @@ as-makeSubset f xs = WitSubset $ \i -> f i (index i xs)+makeSubset f xs = WitSubset $ \i -> f i (indexSing i xs)  -- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied -- predicates.@@ -72,7 +73,7 @@ subsetToList     :: forall f p t. (Universe f, Alternative t)     => (Subset f p --># Any f p) t-subsetToList xs s = getAlt $ (`ifoldMapUni` xs) $ \i _ -> Alt $ case runWitSubset s i of+subsetToList xs s = getAlt $ (`ifoldMapSing` xs) $ \i _ -> Alt $ case runWitSubset s i of     Proved p    -> pure $ WitAny i p     Disproved _ -> empty @@ -158,5 +159,5 @@     -> (q --> p)     -> (Subset f p --> Subset f q) mapSubset f g xs = withSingI xs $-    imapSubset (\i -> f (index i xs))-               (\i -> g (index i xs))+    imapSubset (\i -> f (indexSing i xs))+               (\i -> g (indexSing i xs))