decidable 0.1.2.0 → 0.1.3.0

raw patch · 8 files changed

+316/−42 lines, 8 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +14/−1
• decidable.cabal +7/−6
• src/Data/Type/Predicate.hs +17/−3
• src/Data/Type/Predicate/Auto.hs +42/−0
• src/Data/Type/Predicate/Logic.hs +10/−5
• src/Data/Type/Predicate/Param.hs +41/−0
• src/Data/Type/Universe.hs +184/−26
• src/Data/Type/Universe/Subset.hs +1/−1

@@ -1,6 +1,19 @@ Changelog ========= +Version 0.1.3.0+---------------++*October 24, 2018*++<https://github.com/mstksg/decidable/releases/tag/v0.1.3.0>++*   Added a type and `Universe` for universe disjunction or summing, `:+:`,+    with appropriate `Elem` and `Auto` instances.+*   Added `Universe` instances (and appropriate `Elem` and `Auto` instances)+    for `Proxy` (the null universe) and `Identity`.+*   `Auto` instances for `IsNothing` and `IsLeft`.+ Version 0.1.2.0 --------------- @@ -25,7 +38,7 @@     module documentation for a detailed list of new rules and classes in this     version. *   Convenient combinators for dealing with `Refuted` and `Decision` added to-    *Data.Type.Predicate*: `elimDisproof` and `mapRefuted.+    *Data.Type.Predicate*: `elimDisproof` and `mapRefuted`.   Version 0.1.1.0

@@ -1,11 +1,13 @@--- This file has been generated from package.yaml by hpack version 0.28.2.+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.0. -- -- see: https://github.com/sol/hpack ----- hash: 81cda78c02736265f023817475cdcf593f3a1cd1d8601f09bf92e4719d064fc1+-- hash: 5deeebc3dd1fcd483724e8469079eba0875cd3698198d81352d5b3bd6c2696ef  name:           decidable-version:        0.1.2.0+version:        0.1.3.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,10 +24,9 @@ license-file:   LICENSE tested-with:    GHC >= 8.4 && < 8.8 build-type:     Simple-cabal-version:  >= 1.10 extra-source-files:-    CHANGELOG.md     README.md+    CHANGELOG.md  source-repository head   type: git@@ -44,7 +45,7 @@       Paths_decidable   hs-source-dirs:       src-  ghc-options: -Wall -Wredundant-constraints -Wcompat+  ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns   build-depends:       base >=4.11 && <5     , singletons >=2.4

@@ -132,9 +132,17 @@ -- -- Could also be defined as @'ConstSym1' Void@, but this defintion gives -- us a free 'Decidable' instance.+--+-- @+-- 'Impossible' :: 'Predicate' k+-- @ type Impossible = (Not Evident :: Predicate k)  -- | @'EqualTo' a@ is a predicate that the input is equal to @a@.+--+-- @+-- 'EqualTo' :: k -> 'Predicate' k+-- @ type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)  -- | Convert a tradtional @k ~> 'Bool'@ predicate into a 'Predicate'.@@ -142,7 +150,7 @@ -- @ -- 'BoolPred' :: (k ~> Bool) -> Predicate k -- @-type BoolPred (p :: k ~> Bool) = (EqualTo 'True .@#@$$$ p :: Predicate k)+type BoolPred (p :: k ~> Bool) = (PMap p (EqualTo 'True) :: Predicate k)  -- | Pre-compose a function to a predicate --@@ -271,6 +279,9 @@ -- 'Type'@ instead of matchable type-level functions (that are @k ~> -- 'Type'@). --+-- Mostly is in this library for compatiblity with "traditional" predicates+-- that are GADT type constructors.+-- -- @since 0.1.1.0 type DecidableTC p = Decidable (TyPred p) @@ -291,6 +302,9 @@ -- Is essentially 'Provable', except with /type constructors/ @k -> 'Type'@ -- instead of matchable type-level functions (that are @k ~> 'Type'@). --+-- Mostly is in this library for compatiblity with "traditional" predicates+-- that are GADT type constructors.+-- -- @since 0.1.1.0 type ProvableTC  p = Provable  (TyPred p) @@ -318,10 +332,10 @@     prove = id  instance (Decidable p, SingI f) => Decidable (PMap f p) where-    decide = decide @p . ((sing :: Sing f) @@)+    decide = decide @p . applySing (sing :: Sing f)  instance (Provable p, SingI f) => Provable (PMap f p) where-    prove = prove @p . ((sing :: Sing f) @@)+    prove = prove @p . applySing (sing :: Sing f)  -- | Compose two implications. compImpl

@@ -38,6 +38,7 @@   , autoAny, autoNotAll   ) where +import           Data.Functor.Identity import           Data.List.NonEmpty                 (NonEmpty(..)) import           Data.Singletons import           Data.Singletons.Sigma@@ -169,6 +170,15 @@ -- 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 @@ -216,6 +226,18 @@ 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@@ -228,10 +250,18 @@ instance SingI a => Auto IsJust ('Just a) where     auto = WitAny IJust sing +-- | @since 0.1.3.0+instance Auto IsNothing 'Nothing where+    auto = \case WitAny i _ -> case i of {}+ -- | @since 0.1.2.0 instance SingI a => Auto IsRight ('Right a) where     auto = WitAny IRight sing +-- | @since 0.1.3.0+instance Auto IsLeft ('Left a) where+    auto = \case WitAny i _ -> case i of {}+ -- | @since 0.1.2.0 instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where     auto = WitAny NEHead sing@@ -239,6 +269,18 @@ -- | @since 0.1.2.0 instance SingI a => Auto (NotNull ((,) j)) '(w, a) where     auto = WitAny ISnd sing++instance Auto (Null Proxy) 'Proxy where+    auto = \case WitAny i _ -> case i of {}++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.

@@ -71,10 +71,13 @@ type instance Apply (p ||| q) a = Either (p @@ a) (q @@ a) infixr 2 ||| +-- | Prefers @p@ over @q@. instance (Decidable p, Decidable q) => Decidable (p ||| q) where     decide (x :: Sing a) = decideOr @p @q @a (decide @p x) (decide @q x)  -- | Decide @p '|||' q@ based on decisions of @p@ and @q@.+--+-- Prefers @p@ over @q@. decideOr     :: forall p q a. ()     => Decision (p @@ a)@@ -86,10 +89,14 @@  -- | Left-biased "or".  In proofs, prioritize a proof of the left side over -- a proof of the right side.+--+-- @since 0.1.2.0 type p ^|| q = p ||| Not p &&& q  -- | Right-biased "or".  In proofs, prioritize a proof of the right side over -- a proof of the left side.+--+-- @since 0.1.2.0 type p ||^ q = p &&& Not q ||| q  -- | @p '^^^' q@ is a predicate that either @p@ and @q@ are true, but not@@ -202,11 +209,9 @@ excludedMiddle :: (p &&& Not p) --> Impossible excludedMiddle _ (p, notP) _ = notP p --- | If only this worked, but darn overlapping instances.  Same for p ==>--- p ||| q and p &&& q ==> p :(--- q) ==>--- instance Provable (p &&& Not p ==> Impossible) where---     prove = excludedMiddle @p+-- | @since 0.1.3.0+instance {-# OVERLAPPING #-} Provable (p &&& Not p ==> Impossible) where+    prove = excludedMiddle @p  -- | If p implies q, then not q implies not p. contrapositive

@@ -1,6 +1,7 @@ {-# LANGUAGE ConstraintKinds      #-} {-# LANGUAGE FlexibleContexts     #-} {-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-} {-# LANGUAGE LambdaCase           #-} {-# LANGUAGE ScopedTypeVariables  #-} {-# LANGUAGE TypeApplications     #-}@@ -30,9 +31,12 @@   , Selectable, select   , Searchable, search   , inPNotNull, notNullInP+  -- * Combining+  , OrP, AndP   ) where  import           Data.Singletons+import           Data.Singletons.Prelude.Tuple import           Data.Singletons.Sigma import           Data.Type.Predicate import           Data.Type.Predicate.Logic@@ -192,3 +196,40 @@     decide = mapDecision (\case WitAny i (x :&: p) -> x :&: WitAny i p  )                          (\case x :&: WitAny i p   -> WitAny i (x :&: p))            . decide @(Any f (Found p))++-- | Disjunction on two 'ParamPred's, with appropriate 'Searchable'+-- instance.  Priority is given to the left predicate.+--+-- @since 0.1.3.0+data OrP :: ParamPred k v -> ParamPred k v -> ParamPred k v+type instance Apply (OrP p q x) y = (p x ||| q x) @@ y++-- | Conjunction on two 'ParamPred's, with appropriate 'Searchable' and+-- 'Selectable' instances.+--+-- @since 0.1.3.0+data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u)+type instance Apply (AndP p q x) '(y, z) = (p x @@ y, q x @@ z)++instance (Searchable p, Searchable q) => Decidable (Found (OrP p q)) where+    decide x = case search @p x of+      Proved (s :&: p) -> Proved $ s :&: Left p+      Disproved vp     -> case search @q x of+        Proved (s :&: q) -> Proved $ s :&: Right q+        Disproved vq     -> Disproved $ \case+          s :&: Left  p -> vp (s :&: p)+          s :&: Right q -> vq (s :&: q)++instance (Searchable p, Searchable q) => Decidable (Found (AndP p q)) where+    decide x = case search @p x of+      Proved (s :&: p) -> case search @q x of+        Proved (t :&: q) -> Proved $ STuple2 s t :&: (p, q)+        Disproved vq     -> Disproved $ \case+          STuple2 _ t :&: (_, q) -> vq $ t :&: q+      Disproved vp     -> Disproved $ \case+        STuple2 s _ :&: (p, _) -> vp $ s :&: p++instance (Selectable p, Selectable q) => Provable (Found (AndP p q)) where+    prove x = case select @p x of+        s :&: p -> case select @q x of+          t :&: q -> STuple2 s t :&: (p, q)

@@ -1,20 +1,21 @@-{-# 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 TypeFamilies        #-}+{-# LANGUAGE TypeInType          #-}+{-# LANGUAGE TypeOperators       #-}  -- | -- Module      : Data.Type.Universe@@ -25,15 +26,15 @@ -- Stability   : experimental -- Portability : non-portable ----- Combinators for working with type-level predicates, along with--- typeclasses for canonical proofs and deciding functions.+-- A type family for "containers", intended for allowing lifting of+-- predicates on @k@ to be predicates on containers @f k@. -- module Data.Type.Universe (   -- * Universe     Elem, In, Universe(..)   -- ** Instances-  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..)-  , CompElem(..)+  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IProxy, IIdentity(..)+  , CompElem(..), SumElem(..)   -- ** Predicates   , All, WitAll(..), NotAll   , Any, WitAny(..), None@@ -43,9 +44,15 @@   -- * Decisions and manipulations   , decideAny, decideAll, genAllA, genAll, igenAll   , foldMapUni, ifoldMapUni, index, pickElem-  -- * Universe Composition-  , (:.:)(..), Sing(SComp), sGetComp, GetComp+  -- * Universe Combination+  , Sing (SComp, SInL, SInR)+  -- ** 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   ) where@@ -54,6 +61,7 @@ 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)@@ -64,6 +72,13 @@ 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 @@ -89,7 +104,7 @@ -- -- This is mostly useful for its 'Decidable' and 'TFunctor' instances, -- which lets you lift predicates on @p@ to predicates on @'Any' f p@.-data Any f :: (k ~> Type) -> (f k ~> Type)+data Any f :: Predicate k -> Predicate (f k) type instance Apply (Any f p) as = WitAny f p as  -- | A @'WitAll' p as@ is a witness that the predicate @p a@ is true for all@@ -103,7 +118,7 @@ -- This is mostly useful for its 'Decidable', 'Provable', and 'TFunctor' -- instances, which lets you lift predicates on @p@ to predicates on @'All' -- f p@.-data All f :: (k ~> Type) -> (f k ~> Type)+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@@ -473,6 +488,49 @@      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 {}++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++type instance Elem Identity = IIdentity++-- | The single-pointed universe.  Note that this instance is really only+-- usable in /singletons-2.5/ and higher (so GHC 8.6).+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@@ -482,6 +540,8 @@ -- '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)@@ -501,7 +561,7 @@ -- @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 @@ -591,3 +651,101 @@ -- @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

@@ -120,7 +120,7 @@     => ((Subset f p &&& Subset f q) --> Subset f (p &&& q)) intersection _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideAnd @p @q @a --- | Subset union+-- | Subset union (left-biased) union     :: forall f p q. ()     => ((Subset f p &&& Subset f q) --> Subset f (p ||| q))