move to using functor-products, and overall it's not tooooo bad

package.yaml

@@ -33,8 +33,7 @@ dependencies:
 - singletons >= 2.5
 - vinyl
 - microlens
+- functor-products
 
 library:
   source-dirs: src
-  other-modules:
-  - Data.Type.Universe.Internal

src/Data/Type/Predicate/Auto.hs

@@ -167,18 +167,9 @@ instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where
 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 +210,12 @@ instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where
         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 +243,6 @@ instance SingI a => Auto (NotNull ((,) j)) '(w, a) where
 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.
 --

src/Data/Type/Predicate/Param.hs

@@ -44,6 +44,7 @@ import           Data.Singletons
 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

src/Data/Type/Predicate/Quantification.hs

@@ -25,17 +25,13 @@ module Data.Type.Predicate.Quantification (
   , decideAny, idecideAny, decideNone, idecideNone
   -- ** Entailment
   , entailAny, ientailAny, entailAnyF, ientailAnyF
-  -- ** Composition
-  , allComp, compAll
   -- * All
   , All, WitAll(..), NotAll
   -- ** Decision
   , decideAll, idecideAll
   -- ** Entailment
   , entailAll, ientailAll, entailAllF, ientailAllF
   , decideEntailAll, idecideEntailAll
-  -- ** Composition
-  , anyComp, compAny
   -- * Logical interplay
   , allToAny
   , allNotNone, noneAllNot
@@ -45,10 +41,10 @@ module Data.Type.Predicate.Quantification (
 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
-import           Data.Type.Universe.Prod
 
 -- | 'decideNone', but providing an 'Elem'.
 idecideNone
@@ -75,7 +71,7 @@ ientailAny
     => (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@.
@@ -91,7 +87,7 @@ ientailAll
     => (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@.
@@ -125,7 +121,7 @@ entailAnyF
     => (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
@@ -144,7 +140,7 @@ entailAllF
     => (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
@@ -166,7 +162,7 @@ decideEntailAll = dmap @(All f)
 --
 -- @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@.
@@ -185,7 +181,7 @@ notAllAnyNot
     => 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