diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,15 @@
 Changelog
 =========
 
+Version 0.3.1.1
+---------------
+
+*February 27, 2024*
+
+<https://github.com/mstksg/functor-products/releases/tag/v0.3.1.1>
+
+*   Remove upper bounds and deprecated pragmas
+
 Version 0.3.1.0
 ---------------
 
diff --git a/decidable.cabal b/decidable.cabal
--- a/decidable.cabal
+++ b/decidable.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           decidable
-version:        0.3.1.0
+version:        0.3.1.1
 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
@@ -47,9 +47,9 @@
   ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns
   build-depends:
       base >=4.16 && <5
-    , functor-products >=0.1.2 && <0.2
-    , microlens <0.5
-    , singletons >=3.0 && <3.1
-    , singletons-base <3.2
-    , vinyl <0.15
+    , functor-products >=0.1.2
+    , microlens
+    , singletons >=3.0
+    , singletons-base
+    , vinyl
   default-language: Haskell2010
diff --git a/src/Data/Type/Predicate.hs b/src/Data/Type/Predicate.hs
--- a/src/Data/Type/Predicate.hs
+++ b/src/Data/Type/Predicate.hs
@@ -1,17 +1,18 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds     #-}
-{-# LANGUAGE DefaultSignatures   #-}
-{-# LANGUAGE EmptyCase           #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE FlexibleInstances   #-}
-{-# LANGUAGE InstanceSigs        #-}
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeInType          #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- |
 -- Module      : Data.Type.Predicate
@@ -24,49 +25,72 @@
 --
 -- Combinators for working with type-level predicates, along with
 -- typeclasses for canonical proofs and deciding functions.
---
 module Data.Type.Predicate (
-    -- * Predicates
-    Predicate, Wit(..)
-    -- ** Construct Predicates
-  , TyPred, Evident, EqualTo, BoolPred, Impossible, In
-    -- ** Manipulate predicates
-  , PMap, type Not, decideNot
-    -- * Provable Predicates
-  , Prove, type (-->), type (-->#)
-  , Provable(..)
-  , Disprovable, disprove
-  , ProvableTC, proveTC
-  , TFunctor(..)
-  , compImpl
-    -- * Decidable Predicates
-  , Decide, type (-?>), type (-?>#)
-  , Decidable(..)
-  , DecidableTC, decideTC
-  , DFunctor(..)
+  -- * Predicates
+  Predicate,
+  Wit (..),
+
+  -- ** Construct Predicates
+  TyPred,
+  Evident,
+  EqualTo,
+  BoolPred,
+  Impossible,
+  In,
+
+  -- ** Manipulate predicates
+  PMap,
+  type Not,
+  decideNot,
+
+  -- * Provable Predicates
+  Prove,
+  type (-->),
+  type (-->#),
+  Provable (..),
+  Disprovable,
+  disprove,
+  ProvableTC,
+  proveTC,
+  TFunctor (..),
+  compImpl,
+
+  -- * Decidable Predicates
+  Decide,
+  type (-?>),
+  type (-?>#),
+  Decidable (..),
+  DecidableTC,
+  decideTC,
+  DFunctor (..),
+
   -- * Manipulate Decisions
-  , Decision(..)
-  , flipDecision, mapDecision
-  , elimDisproof
-  , forgetDisproof, forgetProof, isProved, isDisproved
-  , mapRefuted
-  ) where
+  Decision (..),
+  flipDecision,
+  mapDecision,
+  elimDisproof,
+  forgetDisproof,
+  forgetProof,
+  isProved,
+  isDisproved,
+  mapRefuted,
+) where
 
-import           Data.Either.Singletons
-import           Data.Function.Singletons
-import           Data.Functor.Identity
-import           Data.Functor.Identity.Singletons
-import           Data.Kind
-import           Data.List.NonEmpty               (NonEmpty(..))
-import           Data.List.Singletons hiding      (ElemSym1)
-import           Data.Maybe
-import           Data.Maybe.Singletons
-import           Data.Singletons
-import           Data.Singletons.Decide
-import           Data.Tuple.Singletons
-import           Data.Type.Functor.Product
-import           Data.Void
-import qualified Data.List.NonEmpty.Singletons    as NE
+import Data.Either.Singletons
+import Data.Function.Singletons
+import Data.Functor.Identity
+import Data.Functor.Identity.Singletons
+import Data.Kind
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty.Singletons as NE
+import Data.List.Singletons hiding (ElemSym1)
+import Data.Maybe
+import Data.Maybe.Singletons
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Tuple.Singletons
+import Data.Type.Functor.Product
+import Data.Void
 
 -- | A type-level predicate in Haskell.  We say that the predicate @P ::
 -- 'Predicate' k@ is true/satisfied by input @x :: k@ if there exists
@@ -139,6 +163,7 @@
 -- 'Evident' :: 'Predicate' k
 -- @
 data Evident :: Predicate k
+
 type instance Apply Evident a = Sing a
 
 -- | The always-false predicate
@@ -177,7 +202,7 @@
 --
 -- It essentially turns a @k ~> 'Type'@ ("matchable" @'Predicate' k@) /back
 -- into/ a @k -> 'Type'@ predicate.
-newtype Wit p a = Wit { getWit :: p @@ a }
+newtype Wit p a = Wit {getWit :: p @@ a}
 
 -- | A decision function for predicate @p@.  See 'Decidable' for more
 -- information.
@@ -224,22 +249,21 @@
 --     transformers (predicates parameterized on other predicates) easily,
 --     by refering to 'Decidable' instances of the transformed predicates.
 class Decidable p where
-    -- | The canonical decision function for predicate @p@.
-    --
-    -- Note that 'decide' is ambiguously typed, so you /always/ need to call by
-    -- specifying the predicate you want to prove using TypeApplications
-    -- syntax:
-    --
-    -- @
-    -- 'decide' \@MyPredicate
-    -- @
-    --
-    -- See 'decideTC' and 'DecidableTC' for a version that isn't ambiguously
-    -- typed, but only works when @p@ is a type constructor.
-    decide :: Decide p
-
-    default decide :: Provable p => Decide p
-    decide = Proved . prove @p
+  -- | The canonical decision function for predicate @p@.
+  --
+  -- Note that 'decide' is ambiguously typed, so you /always/ need to call by
+  -- specifying the predicate you want to prove using TypeApplications
+  -- syntax:
+  --
+  -- @
+  -- 'decide' \@MyPredicate
+  -- @
+  --
+  -- See 'decideTC' and 'DecidableTC' for a version that isn't ambiguously
+  -- typed, but only works when @p@ is a type constructor.
+  decide :: Decide p
+  default decide :: Provable p => Decide p
+  decide = Proved . prove @p
 
 -- | A typeclass for provable predicates (constructivist tautologies).  In
 -- some context, these are also known as "views".
@@ -263,20 +287,20 @@
 --     transformers (predicates parameterized on other predicates) easily,
 --     by refering to 'Provable' instances of the transformed predicates.
 class Provable p where
-    -- | The canonical proving function for predicate @p@ (or a canonical
-    -- view function for view @p@).
-    --
-    -- Note that 'prove' is ambiguously typed, so you /always/ need to call
-    -- by specifying the predicate you want to prove using TypeApplications
-    -- syntax:
-    --
-    -- @
-    -- 'prove' \@MyPredicate
-    -- @
-    --
-    -- See 'proveTC' and 'ProvableTC' for a version that isn't ambiguously
-    -- typed, but only works when @p@ is a type constructor.
-    prove :: Prove p
+  -- | The canonical proving function for predicate @p@ (or a canonical
+  -- view function for view @p@).
+  --
+  -- Note that 'prove' is ambiguously typed, so you /always/ need to call
+  -- by specifying the predicate you want to prove using TypeApplications
+  -- syntax:
+  --
+  -- @
+  -- 'prove' \@MyPredicate
+  -- @
+  --
+  -- See 'proveTC' and 'ProvableTC' for a version that isn't ambiguously
+  -- typed, but only works when @p@ is a type constructor.
+  prove :: Prove p
 
 -- | @'Disprovable' p@ is a constraint that @p@ can be disproven.
 type Disprovable p = Provable (Not p)
@@ -337,7 +361,7 @@
 -- that are GADT type constructors.
 --
 -- @since 0.1.1.0
-type ProvableTC  p = Provable  (TyPred p)
+type ProvableTC p = Provable (TyPred p)
 
 -- | The canonical proving function for @'DecidableTC' t@.
 --
@@ -352,162 +376,181 @@
 -- | Implicatons @p '-?>' q@ can be lifted "through" a 'DFunctor' into an
 -- @f p '-?>' f q@.
 class DFunctor f where
-    dmap :: forall p q. (p -?> q) -> (f p -?> f q)
+  dmap :: forall p q. (p -?> q) -> (f p -?> f q)
 
 -- | Implicatons @p '-->' q@ can be lifted "through" a 'TFunctor' into an
 -- @f p '-->' f q@.
 class TFunctor f where
-    tmap :: forall p q. (p --> q) -> (f p --> f q)
+  tmap :: forall p q. (p --> q) -> (f p --> f q)
 
 instance (SDecide k, SingI (a :: k)) => Decidable (EqualTo a) where
-    decide = (sing %~)
+  decide = (sing %~)
 
 instance Decidable Evident
 instance Provable Evident where
-    prove = id
+  prove = id
 
 -- | @since 3.0.0
 instance Decidable (TyPred WrappedSing)
+
 -- | @since 3.0.0
 instance Provable (TyPred WrappedSing) where
-    prove = WrapSing
-
+  prove = WrapSing
 
 -- | @since 3.0.0
 instance Provable p => Provable (TyPred (Rec (Wit p))) where
-    prove = mapProd (Wit . prove @p) . singProd
+  prove = mapProd (Wit . prove @p) . singProd
+
 -- | @since 3.0.0
 instance Decidable p => Decidable (TyPred (Rec (Wit p))) where
-    decide = \case
-      SNil         -> Proved RNil
-      x `SCons` xs -> case decide @p x of
-        Proved p -> case decideTC xs of
-          Proved ps -> Proved $ Wit p :& ps
-          Disproved vs -> Disproved $ \case
-            _ :& ps -> vs ps
-        Disproved v -> Disproved $ \case
-          Wit p :& _ -> v p
+  decide = \case
+    SNil -> Proved RNil
+    x `SCons` xs -> case decide @p x of
+      Proved p -> case decideTC xs of
+        Proved ps -> Proved $ Wit p :& ps
+        Disproved vs -> Disproved $ \case
+          _ :& ps -> vs ps
+      Disproved v -> Disproved $ \case
+        Wit p :& _ -> v p
 
 -- | @since 3.0.0
 instance Provable (TyPred (Rec WrappedSing)) where
-    prove = mapProd WrapSing . singProd
+  prove = mapProd WrapSing . singProd
+
 -- | @since 3.0.0
 instance Decidable (TyPred (Rec WrappedSing))
 
 -- | @since 3.0.0
 instance Provable p => Provable (TyPred (PMaybe (Wit p))) where
-    prove = mapProd (Wit . prove @p) . singProd
+  prove = mapProd (Wit . prove @p) . singProd
+
 -- | @since 3.0.0
 instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where
-    decide = \case
-      SNothing -> Proved PNothing
-      SJust x  -> mapDecision (PJust . Wit) (\case PJust (Wit p) -> p)
-                . decide @p
-                $ x
+  decide = \case
+    SNothing -> Proved PNothing
+    SJust x ->
+      mapDecision (PJust . Wit) (\case PJust (Wit p) -> p)
+        . decide @p
+        $ x
 
 -- | @since 3.0.0
 instance Provable (TyPred (PMaybe WrappedSing)) where
-    prove = mapProd WrapSing . singProd
+  prove = mapProd WrapSing . singProd
+
 -- | @since 3.0.0
 instance Decidable (TyPred (PMaybe WrappedSing))
 
 -- | @since 3.0.0
 instance Provable p => Provable (TyPred (NERec (Wit p))) where
-    prove = mapProd (Wit . prove @p) . singProd
+  prove = mapProd (Wit . prove @p) . singProd
+
 -- | @since 3.0.0
 instance Decidable p => Decidable (TyPred (NERec (Wit p))) where
-    decide = \case
-      x NE.:%| xs -> case decide @p x of
-        Proved p -> case decideTC xs of
-          Proved ps -> Proved $ Wit p :&| ps
-          Disproved vs -> Disproved $ \case
-            _ :&| ps -> vs ps
-        Disproved v -> Disproved $ \case
-          Wit p :&| _ -> v p
+  decide = \case
+    x NE.:%| xs -> case decide @p x of
+      Proved p -> case decideTC xs of
+        Proved ps -> Proved $ Wit p :&| ps
+        Disproved vs -> Disproved $ \case
+          _ :&| ps -> vs ps
+      Disproved v -> Disproved $ \case
+        Wit p :&| _ -> v p
 
 -- | @since 3.0.0
 instance Provable (TyPred (NERec WrappedSing)) where
-    prove = mapProd WrapSing . singProd
+  prove = mapProd WrapSing . singProd
+
 -- | @since 3.0.0
 instance Decidable (TyPred (NERec WrappedSing))
 
 -- | @since 3.0.0
 instance Provable p => Provable (TyPred (PIdentity (Wit p))) where
-    prove = mapProd (Wit . prove @p) . singProd
+  prove = mapProd (Wit . prove @p) . singProd
+
 -- | @since 3.0.0
 instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where
-    decide = \case
-      SIdentity x -> mapDecision (PIdentity . Wit) (\case PIdentity (Wit p) -> p)
-                   . decide @p
-                   $ x
+  decide = \case
+    SIdentity x ->
+      mapDecision (PIdentity . Wit) (\case PIdentity (Wit p) -> p)
+        . decide @p
+        $ x
 
 -- | @since 3.0.0
 instance Provable (TyPred (PIdentity WrappedSing)) where
-    prove = mapProd WrapSing . singProd
+  prove = mapProd WrapSing . singProd
+
 -- | @since 3.0.0
 instance Decidable (TyPred (PIdentity WrappedSing))
 
 -- | @since 3.0.0
 instance Provable p => Provable (TyPred (PEither (Wit p))) where
-    prove = mapProd (Wit . prove @p) . singProd
+  prove = mapProd (Wit . prove @p) . singProd
+
 -- | @since 3.0.0
 instance Decidable p => Decidable (TyPred (PEither (Wit p))) where
-    decide = \case
-      SLeft  x -> Proved $ PLeft x
-      SRight y -> mapDecision (PRight . Wit) (\case PRight (Wit p) -> p)
-                . decide @p
-                $ y
+  decide = \case
+    SLeft x -> Proved $ PLeft x
+    SRight y ->
+      mapDecision (PRight . Wit) (\case PRight (Wit p) -> p)
+        . decide @p
+        $ y
 
 -- | @since 3.0.0
 instance Provable (TyPred (PEither WrappedSing)) where
-    prove = mapProd WrapSing . singProd
+  prove = mapProd WrapSing . singProd
+
 -- | @since 3.0.0
 instance Decidable (TyPred (PEither WrappedSing))
 
 -- | @since 3.0.0
 instance Provable p => Provable (TyPred (PTup (Wit p))) where
-    prove = mapProd (Wit . prove @p) . singProd
+  prove = mapProd (Wit . prove @p) . singProd
+
 -- | @since 3.0.0
 instance Decidable p => Decidable (TyPred (PTup (Wit p))) where
-    decide (STuple2 x y) = mapDecision (PTup x . Wit) (\case PTup _ (Wit p) -> p)
-                         . decide @p
-                         $ y
+  decide (STuple2 x y) =
+    mapDecision (PTup x . Wit) (\case PTup _ (Wit p) -> p)
+      . decide @p
+      $ y
 
 -- | @since 3.0.0
 instance Provable (TyPred (PTup WrappedSing)) where
-    prove = mapProd WrapSing . singProd
+  prove = mapProd WrapSing . singProd
+
 -- | @since 3.0.0
 instance Decidable (TyPred (PTup WrappedSing))
 
 instance (Decidable p, SingI f) => Decidable (PMap f p) where
-    decide = decide @p . applySing (sing :: Sing f)
+  decide = decide @p . applySing (sing :: Sing f)
 
 instance (Provable p, SingI f) => Provable (PMap f p) where
-    prove = prove @p . applySing (sing :: Sing f)
+  prove = prove @p . applySing (sing :: Sing f)
 
 -- | Compose two implications.
-compImpl
-    :: forall p q r. ()
-    => p --> q
-    -> q --> r
-    -> p --> r
+compImpl ::
+  forall p q r.
+  () =>
+  p --> q ->
+  q --> r ->
+  p --> r
 compImpl f g s = g s . f s
 
 -- | @'Not' p@ is the predicate that @p@ is not true.
 data Not :: Predicate k -> Predicate k
+
 type instance Apply (Not p) a = Refuted (p @@ a)
 
 instance Decidable p => Decidable (Not p) where
-    decide (x :: Sing a) = decideNot @p @a (decide @p x)
+  decide (x :: Sing a) = decideNot @p @a (decide @p x)
 
 instance Provable (Not Impossible) where
-    prove x v = absurd $ v x
+  prove x v = absurd $ v x
 
 -- | Decide @'Not' p@ based on decisions of @p@.
-decideNot
-    :: forall p a. ()
-    => Decision (p @@ a)
-    -> Decision (Not p @@ a)
+decideNot ::
+  forall p a.
+  () =>
+  Decision (p @@ a) ->
+  Decision (Not p @@ a)
 decideNot = flipDecision
 
 -- | Flip the contents of a decision.  Turn a proof of @a@ into a disproof
@@ -517,42 +560,42 @@
 -- 'Data.Type.Predicate.Logic.doubleNegation' for a situation where it is.
 --
 -- @since 0.1.1.0
-flipDecision
-    :: Decision a
-    -> Decision (Refuted a)
+flipDecision ::
+  Decision a ->
+  Decision (Refuted a)
 flipDecision = \case
-    Proved    p -> Disproved ($ p)
-    Disproved v -> Proved v
+  Proved p -> Disproved ($ p)
+  Disproved v -> Proved v
 
 -- | Map over the value inside a 'Decision'.
-mapDecision
-    :: (a -> b)
-    -> (b -> a)
-    -> Decision a
-    -> Decision b
+mapDecision ::
+  (a -> b) ->
+  (b -> a) ->
+  Decision a ->
+  Decision b
 mapDecision f g = \case
-    Proved    p -> Proved    $ f p
-    Disproved v -> Disproved $ mapRefuted g v
+  Proved p -> Proved $ f p
+  Disproved v -> Disproved $ mapRefuted g v
 
 -- | Converts a 'Decision' to a 'Maybe'.  Drop the witness of disproof of
 -- @a@, returning 'Just' if 'Proved' (with the proof) and 'Nothing' if
 -- 'Disproved'.
 --
 -- @since 0.1.1.0
-forgetDisproof
-    :: Decision a
-    -> Maybe a
+forgetDisproof ::
+  Decision a ->
+  Maybe a
 forgetDisproof = \case
-    Proved    p -> Just p
-    Disproved _ -> Nothing
+  Proved p -> Just p
+  Disproved _ -> Nothing
 
 -- | Drop the witness of proof of @a@, returning 'Nothing' if 'Proved' and
 -- 'Just' if 'Disproved' (with the disproof).
 --
 -- @since 0.1.1.0
-forgetProof
-    :: Decision a
-    -> Maybe (Refuted a)
+forgetProof ::
+  Decision a ->
+  Maybe (Refuted a)
 forgetProof = forgetDisproof . flipDecision
 
 -- | Boolean test if a 'Decision' is 'Proved'.
@@ -571,22 +614,22 @@
 -- branch of 'Decision' to certaintify the proof.
 --
 -- @since 0.1.2.0
-elimDisproof
-    :: Decision a
-    -> Refuted (Refuted a)
-    -> a
+elimDisproof ::
+  Decision a ->
+  Refuted (Refuted a) ->
+  a
 elimDisproof = \case
-    Proved    p -> const p
-    Disproved v -> absurd . ($ v)
+  Proved p -> const p
+  Disproved v -> absurd . ($ v)
 
 -- | Change the target of a 'Refuted' with a contravariant mapping
 -- function.
 --
 -- @since 0.1.2.0
-mapRefuted
-    :: (a -> b)
-    -> Refuted b
-    -> Refuted a
+mapRefuted ::
+  (a -> b) ->
+  Refuted b ->
+  Refuted a
 mapRefuted = flip (.)
 
 -- | @'In' f as@ is a predicate that a given input @a@ is a member of
@@ -594,52 +637,52 @@
 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
+  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
+  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
+  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
+  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
+  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
+  decide x = case sing @as of
+    SIdentity y -> case x %~ y of
+      Proved Refl -> Proved IId
+      Disproved v -> Disproved $ \case IId -> v Refl
diff --git a/src/Data/Type/Predicate/Auto.hs b/src/Data/Type/Predicate/Auto.hs
--- a/src/Data/Type/Predicate/Auto.hs
+++ b/src/Data/Type/Predicate/Auto.hs
@@ -1,17 +1,17 @@
-{-# LANGUAGE AllowAmbiguousTypes   #-}
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE EmptyCase             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE KindSignatures        #-}
-{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeInType            #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 -- |
 -- Module      : Data.Type.Predicate.Auto
@@ -28,28 +28,30 @@
 -- @since 0.1.1.0
 module Data.Type.Predicate.Auto (
   -- * Automatically generate witnesses at compile-time
-    Auto(..)
-  , autoTC
-  , AutoNot
-  , autoNot
-  , autoAny, autoNotAll
-  , AutoProvable
+  Auto (..),
+  autoTC,
+  AutoNot,
+  autoNot,
+  autoAny,
+  autoNotAll,
+  AutoProvable,
+
   -- ** Helper classes
-  , AutoElem(..)
-  , AutoAll(..)
-  ) where
+  AutoElem (..),
+  AutoAll (..),
+) where
 
-import           Data.Functor.Identity
-import           Data.List.NonEmpty                 (NonEmpty(..))
-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
-import           Data.Type.Predicate.Quantification
-import           Data.Type.Universe
+import Data.Functor.Identity
+import Data.List.NonEmpty (NonEmpty (..))
+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
+import Data.Type.Predicate.Quantification
+import Data.Type.Universe
 
 -- | Automatically generate a witness for predicate @p@ applied to input
 -- @a@.
@@ -76,14 +78,14 @@
 -- For these, the compiler needs help; you can use 'autoAny' and
 -- 'autoNotAll' for these situations.
 class Auto (p :: Predicate k) (a :: k) where
-    -- | Have the compiler generate a witness for @p \@\@ a@.
-    --
-    -- Must be called using type application syntax:
-    --
-    -- @
-    -- 'auto' @_ @p @a
-    -- @
-    auto :: p @@ a
+  -- | Have the compiler generate a witness for @p \@\@ a@.
+  --
+  -- Must be called using type application syntax:
+  --
+  -- @
+  -- 'auto' @_ @p @a
+  -- @
+  auto :: p @@ a
 
 -- | A version of 'auto' that "just works" with type inference, if the
 -- predicate is a type constructor.
@@ -93,20 +95,20 @@
 autoTC = auto @_ @(TyPred t) @a
 
 instance SingI a => Auto Evident a where
-    auto = sing
+  auto = sing
 
 -- | @since 0.1.2.0
 instance SingI a => Auto (Not Impossible) a where
-    auto = ($ sing)
+  auto = ($ sing)
 
 instance Auto (EqualTo a) a where
-    auto = Refl
+  auto = Refl
 
 instance (Auto p a, Auto q a) => Auto (p &&& q) a where
-    auto = (auto @_ @p @a, auto @_ @q @a)
+  auto = (auto @_ @p @a, auto @_ @q @a)
 
 instance Auto q a => Auto (p ==> q) a where
-    auto _ = auto @_ @q @a
+  auto _ = auto @_ @q @a
 
 -- | Helper "predicate transformer" that gives you an instant 'auto' for
 -- any 'Provable' instance.
@@ -123,10 +125,11 @@
 --
 -- 'AutoProvable' is essentially the identity function.
 data AutoProvable :: Predicate k -> Predicate k
+
 type instance Apply (AutoProvable p) a = p @@ a
 
 instance (Provable p, SingI a) => Auto (AutoProvable p) a where
-    auto = prove @p @a sing
+  auto = prove @p @a sing
 
 -- | Typeclass representing 'Elem's pointing to an @a :: k@ that can be
 -- generated automatically from type-level collection @as :: f k@.
@@ -150,37 +153,37 @@
 -- -- IS (IS IZ)
 -- @
 class AutoElem f (as :: f k) (a :: k) where
-    -- | Generate the 'Elem' pointing to the @a :: @ in a type-level
-    -- collection @as :: f k@.
-    autoElem :: Elem f as a
+  -- | Generate the 'Elem' pointing to the @a :: @ in a type-level
+  -- collection @as :: f k@.
+  autoElem :: Elem f as a
 
 instance {-# OVERLAPPING #-} AutoElem [] (a ': as) a where
-    autoElem = IZ
+  autoElem = IZ
 
 instance {-# OVERLAPPING #-} AutoElem [] as a => AutoElem [] (b ': as) a where
-    autoElem = IS autoElem
+  autoElem = IS autoElem
 
 instance AutoElem Maybe ('Just a) a where
-    autoElem = IJust
+  autoElem = IJust
 
 instance AutoElem (Either j) ('Right a) a where
-    autoElem = IRight
+  autoElem = IRight
 
 instance AutoElem NonEmpty (a ':| as) a where
-    autoElem = NEHead
+  autoElem = NEHead
 
 instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where
-    autoElem = NETail autoElem
+  autoElem = NETail autoElem
 
 -- | @since 0.1.2.0
 instance AutoElem ((,) j) '(w, a) a where
-    autoElem = ISnd
+  autoElem = ISnd
 
 instance AutoElem Identity ('Identity a) a where
-    autoElem = IId
+  autoElem = IId
 
 instance AutoElem f as a => Auto (In f as) a where
-    auto = autoElem @_ @f @as @a
+  auto = autoElem @_ @f @as @a
 
 -- | Helper class for deriving 'Auto' instances for 'All' predicates; each
 -- 'Universe' instance is expected to implement these if possible, to get
@@ -191,66 +194,66 @@
 --
 -- @since 0.1.2.0
 class AutoAll f (p :: Predicate k) (as :: f k) where
-    -- | Generate an 'All' for a given predicate over all items in @as@.
-    autoAll :: All f p @@ as
+  -- | Generate an 'All' for a given predicate over all items in @as@.
+  autoAll :: All f p @@ as
 
 instance AutoAll [] p '[] where
-    autoAll = WitAll $ \case {}
+  autoAll = WitAll $ \case {}
 
 instance (Auto p a, AutoAll [] p as) => AutoAll [] p (a ': as) where
-    autoAll = WitAll $ \case
-        IZ   -> auto @_ @p @a
-        IS i -> runWitAll (autoAll @_ @[] @p @as) i
+  autoAll = WitAll $ \case
+    IZ -> auto @_ @p @a
+    IS i -> runWitAll (autoAll @_ @[] @p @as) i
 
 instance AutoAll Maybe p 'Nothing where
-    autoAll = WitAll $ \case {}
+  autoAll = WitAll $ \case {}
 
 instance Auto p a => AutoAll Maybe p ('Just a) where
-    autoAll = WitAll $ \case IJust -> auto @_ @p @a
+  autoAll = WitAll $ \case IJust -> auto @_ @p @a
 
 instance AutoAll (Either j) p ('Left e) where
-    autoAll = WitAll $ \case {}
+  autoAll = WitAll $ \case {}
 
 instance Auto p a => AutoAll (Either j) p ('Right a) where
-    autoAll = WitAll $ \case IRight -> auto @_ @p @a
+  autoAll = WitAll $ \case IRight -> auto @_ @p @a
 
 instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where
-    autoAll = WitAll $ \case
-        NEHead   -> auto @_ @p @a
-        NETail i -> runWitAll (autoAll @_ @[] @p @as) i
+  autoAll = WitAll $ \case
+    NEHead -> auto @_ @p @a
+    NETail i -> runWitAll (autoAll @_ @[] @p @as) i
 
 instance Auto p a => AutoAll ((,) j) p '(w, a) where
-    autoAll = WitAll $ \case ISnd -> auto @_ @p @a
+  autoAll = WitAll $ \case ISnd -> auto @_ @p @a
 
 instance Auto p a => AutoAll Identity p ('Identity a) where
-    autoAll = WitAll $ \case IId -> auto @_ @p @a
+  autoAll = WitAll $ \case IId -> auto @_ @p @a
 
 -- | @since 0.1.2.0
 instance AutoAll f p as => Auto (All f p) as where
-    auto = autoAll @_ @f @p @as
+  auto = autoAll @_ @f @p @as
 
 -- | @since 0.1.2.0
 instance SingI a => Auto (NotNull []) (a ': as) where
-    auto = WitAny IZ sing
+  auto = WitAny IZ sing
 
 -- | @since 0.1.2.0
 instance SingI a => Auto IsJust ('Just a) where
-    auto = WitAny IJust sing
+  auto = WitAny IJust sing
 
 -- | @since 0.1.2.0
 instance SingI a => Auto IsRight ('Right a) where
-    auto = WitAny IRight sing
+  auto = WitAny IRight sing
 
 -- | @since 0.1.2.0
 instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where
-    auto = WitAny NEHead sing
+  auto = WitAny NEHead sing
 
 -- | @since 0.1.2.0
 instance SingI a => Auto (NotNull ((,) j)) '(w, a) where
-    auto = WitAny ISnd sing
+  auto = WitAny ISnd sing
 
 instance SingI a => Auto (NotNull Identity) ('Identity a) where
-    auto = WitAny IId sing
+  auto = WitAny IId sing
 
 -- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to
 -- not be true at compiletime.
@@ -270,21 +273,22 @@
 
 -- | @since 0.1.2.0
 instance Auto (Found p) (f @@ a) => Auto (Found (PPMap f p)) a where
-    auto = case auto @_ @(Found p) @(f @@ a) of
-        i :&: p -> i :&: p
+  auto = case auto @_ @(Found p) @(f @@ a) of
+    i :&: p -> i :&: p
 
 -- | @since 0.1.2.0
 instance Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p)) a where
-    auto = mapRefuted (\(i :&: p) -> i :&: p)
-         $ autoNot @_ @(Found p) @(f @@ a)
+  auto =
+    mapRefuted (\(i :&: p) -> i :&: p) $
+      autoNot @_ @(Found p) @(f @@ a)
 
 -- | @since 0.1.2.0
 instance Auto p (f @@ a) => Auto (PMap f p) a where
-    auto = auto @_ @p @(f @@ a)
+  auto = auto @_ @p @(f @@ a)
 
 -- | @since 0.1.2.0
 instance AutoNot p (f @@ a) => Auto (Not (PMap f p)) a where
-    auto = autoNot @_ @p @(f @@ a)
+  auto = autoNot @_ @p @(f @@ a)
 
 -- | Helper function to generate an @'Any' f p@ if you can pick out
 -- a specific @a@ in @as@ where the predicate is provable at compile-time.
@@ -293,15 +297,16 @@
 -- a Haskell typeclass.
 --
 -- @since 0.1.2.0
-autoAny
-    :: forall f p as a. Auto p a
-    => Elem f as a
-    -> Any f p @@ as
+autoAny ::
+  forall f p as a.
+  Auto p a =>
+  Elem f as a ->
+  Any f p @@ as
 autoAny i = WitAny i (auto @_ @p @a)
 
 -- | @since 0.1.2.0
 instance (SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p)) as where
-    auto = allNotNone sing $ autoAll @_ @f @(Not p) @as
+  auto = allNotNone sing $ autoAll @_ @f @(Not p) @as
 
 -- | Helper function to generate a @'Not' ('All' f p)@ if you can pick out
 -- a specific @a@ in @as@ where the predicate is disprovable at compile-time.
@@ -310,51 +315,63 @@
 -- a Haskell typeclass.
 --
 -- @since 0.1.2.0
-autoNotAll
-    :: forall p f as a. (AutoNot p a, SingI as)
-    => Elem f as a
-    -> Not (All f p) @@ as
+autoNotAll ::
+  forall p f as a.
+  (AutoNot p a, SingI as) =>
+  Elem f as a ->
+  Not (All f p) @@ as
 autoNotAll = anyNotNotAll sing . autoAny
 
 -- | @since 0.1.2.0
 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
+  auto =
+    mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p)) $
+      auto @_ @(Not (Any f (Found p))) @as
 
 -- | @since 3.0.0
 instance SingI as => Auto (TyPred (Rec WrappedSing)) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance SingI as => Auto (TyPred (PMaybe WrappedSing)) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance SingI as => Auto (TyPred (NERec WrappedSing)) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance SingI as => Auto (TyPred (PEither WrappedSing)) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance SingI as => Auto (TyPred (PTup WrappedSing)) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance SingI as => Auto (TyPred (PIdentity WrappedSing)) as where
-    auto = proveTC sing
+  auto = proveTC sing
 
 -- | @since 3.0.0
 instance (SingI as, Provable p) => Auto (TyPred (Rec (Wit p))) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance (SingI as, Provable p) => Auto (TyPred (PMaybe (Wit p))) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance (SingI as, Provable p) => Auto (TyPred (NERec (Wit p))) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance (SingI as, Provable p) => Auto (TyPred (PEither (Wit p))) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance (SingI as, Provable p) => Auto (TyPred (PTup (Wit p))) as where
-    auto = proveTC sing
+  auto = proveTC sing
+
 -- | @since 3.0.0
 instance (SingI as, Provable p) => Auto (TyPred (PIdentity (Wit p))) as where
-    auto = proveTC sing
+  auto = proveTC sing
diff --git a/src/Data/Type/Predicate/Logic.hs b/src/Data/Type/Predicate/Logic.hs
--- a/src/Data/Type/Predicate/Logic.hs
+++ b/src/Data/Type/Predicate/Logic.hs
@@ -1,15 +1,16 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds     #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE FlexibleInstances   #-}
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections       #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeInType          #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- |
 -- Module      : Data.Type.Predicate.Logic
@@ -24,68 +25,94 @@
 -- logical combinators.
 module Data.Type.Predicate.Logic (
   -- * Top and bottom
-    Evident, Impossible
+  Evident,
+  Impossible,
+
   -- * Logical connectives
-  , type Not, decideNot
-  , type (&&&), decideAnd
-  , type (|||), decideOr, type (^||), type (||^)
-  , type (^^^), decideXor
-  , type (==>), proveImplies, Implies
-  , type (<==>), Equiv
+  type Not,
+  decideNot,
+  type (&&&),
+  decideAnd,
+  type (|||),
+  decideOr,
+  type (^||),
+  type (||^),
+  type (^^^),
+  decideXor,
+  type (==>),
+  proveImplies,
+  Implies,
+  type (<==>),
+  Equiv,
+
   -- * Logical deductions
-  , compImpl, explosion, atom
-  , complementation, doubleNegation, tripleNegation, negateTwice
-  , contrapositive, contrapositive'
+  compImpl,
+  explosion,
+  atom,
+  complementation,
+  doubleNegation,
+  tripleNegation,
+  negateTwice,
+  contrapositive,
+  contrapositive',
+
   -- ** Lattice
-  , projAndFst, projAndSnd, injOrLeft, injOrRight
-  ) where
+  projAndFst,
+  projAndSnd,
+  injOrLeft,
+  injOrRight,
+) where
 
-import           Data.Singletons
-import           Data.Singletons.Decide
-import           Data.Type.Predicate
-import           Data.Void
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Type.Predicate
+import Data.Void
 
 -- | @p '&&&' q@ is a predicate that both @p@ and @q@ are true.
 data (&&&) :: Predicate k -> Predicate k -> Predicate k
+
 type instance Apply (p &&& q) a = (p @@ a, q @@ a)
 infixr 3 &&&
 
 instance (Decidable p, Decidable q) => Decidable (p &&& q) where
-    decide (x :: Sing a) = decideAnd @p @q @a (decide @p x) (decide @q x)
+  decide (x :: Sing a) = decideAnd @p @q @a (decide @p x) (decide @q x)
 
 instance (Provable p, Provable q) => Provable (p &&& q) where
-    prove x = (prove @p x, prove @q x)
+  prove x = (prove @p x, prove @q x)
 
 -- | Decide @p '&&&' q@ based on decisions of @p@ and @q@.
-decideAnd
-    :: forall p q a. ()
-    => Decision (p @@ a)
-    -> Decision (q @@ a)
-    -> Decision ((p &&& q) @@ a)
+decideAnd ::
+  forall p q a.
+  () =>
+  Decision (p @@ a) ->
+  Decision (q @@ a) ->
+  Decision ((p &&& q) @@ a)
 decideAnd = \case
-    Proved p    -> mapDecision (p,) snd
-    Disproved v -> \_ -> Disproved $ \(p, _) -> v p
+  Proved p -> mapDecision (p,) snd
+  Disproved v -> \_ -> Disproved $ \(p, _) -> v p
 
 -- | @p '|||' q@ is a predicate that either @p@ and @q@ are true.
 data (|||) :: Predicate k -> Predicate k -> Predicate k
+
 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 (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)
-    -> Decision (q @@ a)
-    -> Decision ((p ||| q) @@ a)
+decideOr ::
+  forall p q a.
+  () =>
+  Decision (p @@ a) ->
+  Decision (q @@ a) ->
+  Decision ((p ||| q) @@ a)
 decideOr = \case
-    Proved p    -> \_ -> Proved $ Left p
-    Disproved v -> mapDecision Right (either (absurd . v) id)
+  Proved p -> \_ -> Proved $ Left p
+  Disproved v -> mapDecision Right (either (absurd . v) id)
 
 -- | Left-biased "or".  In proofs, prioritize a proof of the left side over
 -- a proof of the right side.
@@ -104,78 +131,87 @@
 type p ^^^ q = (p &&& Not q) ||| (Not p &&& q)
 
 -- | Decide @p '^^^' q@ based on decisions of @p@ and @q@.
-decideXor
-    :: forall p q a. ()
-    => Decision (p @@ a)
-    -> Decision (q @@ a)
-    -> Decision ((p ^^^ q) @@ a)
-decideXor p q = decideOr @(p &&& Not q) @(Not p &&& q) @a
-                  (decideAnd @p @(Not q) @a p (decideNot @q @a q))
-                  (decideAnd @(Not p) @q @a (decideNot @p @a p) q)
+decideXor ::
+  forall p q a.
+  () =>
+  Decision (p @@ a) ->
+  Decision (q @@ a) ->
+  Decision ((p ^^^ q) @@ a)
+decideXor p q =
+  decideOr @(p &&& Not q) @(Not p &&& q) @a
+    (decideAnd @p @(Not q) @a p (decideNot @q @a q))
+    (decideAnd @(Not p) @q @a (decideNot @p @a p) q)
 
 -- | @p ==> q@ is true if @q@ is provably true under the condition that @p@
 -- is true.
 data (==>) :: Predicate k -> Predicate k -> Predicate k
+
 type instance Apply (p ==> q) a = p @@ a -> q @@ a
 
 infixr 1 ==>
 
-instance Decidable (Impossible ==> p) where
+instance Decidable (Impossible ==> p)
 instance Provable (Impossible ==> p) where
-    prove = explosion @p
+  prove = explosion @p
 
 instance (Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p) where
-    decide x = case decide @(p ==> q) x of
-      Proved pq     -> Proved $ \vq p -> vq (pq p)
-      Disproved vpq -> case decide @q x of
-        Proved    q  -> Disproved $ \_     -> vpq (const q)
-        Disproved vq -> Disproved $ \vnpnq -> vpq (absurd . vnpnq vq)
+  decide x = case decide @(p ==> q) x of
+    Proved pq -> Proved $ \vq p -> vq (pq p)
+    Disproved vpq -> case decide @q x of
+      Proved q -> Disproved $ \_ -> vpq (const q)
+      Disproved vq -> Disproved $ \vnpnq -> vpq (absurd . vnpnq vq)
 instance Provable (p ==> q) => Provable (Not q ==> Not p) where
-    prove = contrapositive @p @q (prove @(p ==> q))
+  prove = contrapositive @p @q (prove @(p ==> q))
 
 -- | @since 0.1.1.0
-instance {-# OVERLAPPING #-} Decidable (p &&& q ==> p) where
+instance {-# OVERLAPPING #-} Decidable (p &&& q ==> p)
+
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Provable (p &&& q ==> p) where
-    prove = projAndFst @p @q
+  prove = projAndFst @p @q
 
 -- | @since 0.1.1.0
-instance {-# OVERLAPPING #-} Decidable (p &&& q ==> q) where
+instance {-# OVERLAPPING #-} Decidable (p &&& q ==> q)
+
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Provable (p &&& q ==> q) where
-    prove = projAndSnd @p @q
+  prove = projAndSnd @p @q
 
 -- | @since 0.1.1.0
-instance {-# OVERLAPPING #-} Decidable (p &&& p ==> p) where
+instance {-# OVERLAPPING #-} Decidable (p &&& p ==> p)
+
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Provable (p &&& p ==> p) where
-    prove = projAndFst @p @p
+  prove = projAndFst @p @p
 
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Decidable (p ==> p ||| q)
+
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Provable (p ==> p ||| q) where
-    prove = injOrLeft @p @q
+  prove = injOrLeft @p @q
 
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Decidable (q ==> p ||| q)
+
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Provable (q ==> p ||| q) where
-    prove = injOrRight @p @q
+  prove = injOrRight @p @q
 
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Decidable (p ==> p ||| p)
+
 -- | @since 0.1.1.0
 instance {-# OVERLAPPING #-} Provable (p ==> p ||| p) where
-    prove = injOrLeft @p @p
+  prove = injOrLeft @p @p
 
 -- | @'Implies' p q@ is a constraint that @p '==>' q@ is 'Provable'; that
 -- is, you can prove that @p@ implies @q@.
-type Implies  p q = Provable  (p ==> q)
+type Implies p q = Provable (p ==> q)
 
 -- | @'Equiv' p q@ is a constraint that @p '<==>' q@ is 'Provable'; that
 -- is, you can prove that @p@ is logically equivalent to @q@.
-type Equiv  p q = Provable  (p <==> q)
+type Equiv p q = Provable (p <==> q)
 
 -- | If @q@ is provable, then so is @p '==>' q@.
 --
@@ -193,7 +229,8 @@
 proveImplies q x _ = q x
 
 -- | Two-way implication, or logical equivalence
-type (p <==> q) = p ==> q &&& q ==> p
+type p <==> q = p ==> q &&& q ==> p
+
 infixr 1 <==>
 
 -- | From @'Impossible' @@ a@, you can prove anything.  Essentially
@@ -215,23 +252,24 @@
 
 -- | @since 0.1.3.0
 instance {-# OVERLAPPING #-} Provable (p &&& Not p ==> Impossible) where
-    prove = complementation @p
+  prove = complementation @p
 
 -- | If p implies q, then not q implies not p.
-contrapositive
-    :: (p --> q)
-    -> (Not q --> Not p)
+contrapositive ::
+  (p --> q) ->
+  (Not q --> Not p)
 contrapositive f x vQ p = vQ (f x p)
 
 -- | Reverse direction of 'contrapositive'.  Only possible if @q@ is
 -- 'Decidable' on its own, without the help of @p@, which makes this much
 -- less useful.
-contrapositive'
-    :: forall p q. Decidable q
-    => (Not q --> Not p)
-    -> (p --> q)
+contrapositive' ::
+  forall p q.
+  Decidable q =>
+  (Not q --> Not p) ->
+  (p --> q)
 contrapositive' f x p = elimDisproof (decide @q x) $ \vQ ->
-    f x vQ p
+  f x vQ p
 
 -- | Logical double negation.  Only possible if @p@ is 'Decidable'.
 --
@@ -240,7 +278,7 @@
 -- p)) implies not p (see 'tripleNegation')
 doubleNegation :: forall p. Decidable p => Not (Not p) --> p
 doubleNegation x vvP = elimDisproof (decide @p x) $ \vP ->
-    vvP vP
+  vvP vP
 
 -- | In constructivist logic, not (not (not p)) implies not p.
 --
diff --git a/src/Data/Type/Predicate/Param.hs b/src/Data/Type/Predicate/Param.hs
--- a/src/Data/Type/Predicate/Param.hs
+++ b/src/Data/Type/Predicate/Param.hs
@@ -1,13 +1,14 @@
-{-# LANGUAGE ConstraintKinds      #-}
-{-# LANGUAGE FlexibleContexts     #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE TypeApplications     #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeInType           #-}
-{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- |
@@ -21,33 +22,49 @@
 --
 -- Manipulate "parameterized predicates".  See 'ParamPred' and 'Found' for
 -- more information.
---
 module Data.Type.Predicate.Param (
   -- * Parameterized Predicates
-    ParamPred
-  , IsTC, EqBy
-  , FlipPP, ConstPP, PPMap, PPMapV, InP, AnyMatch, TyPP
+  ParamPred,
+  IsTC,
+  EqBy,
+  FlipPP,
+  ConstPP,
+  PPMap,
+  PPMapV,
+  InP,
+  AnyMatch,
+  TyPP,
+
   -- * Deciding and Proving
-  , Found, NotFound
-  , Selectable, select
-  , Searchable, search
-  , inPNotNull, notNullInP
+  Found,
+  NotFound,
+  Selectable,
+  select,
+  Searchable,
+  search,
+  inPNotNull,
+  notNullInP,
+
   -- ** Type Constructors
-  , SelectableTC, selectTC
-  , SearchableTC, searchTC
+  SelectableTC,
+  selectTC,
+  SearchableTC,
+  searchTC,
+
   -- * Combining
-  , OrP, AndP
-  ) where
+  OrP,
+  AndP,
+) where
 
-import           Data.Kind
-import           Data.Singletons
-import           Data.Singletons.Decide
-import           Data.Singletons.Sigma
-import           Data.Tuple.Singletons
-import           Data.Type.Functor.Product
-import           Data.Type.Predicate
-import           Data.Type.Predicate.Logic
-import           Data.Type.Universe
+import Data.Kind
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Singletons.Sigma
+import Data.Tuple.Singletons
+import Data.Type.Functor.Product
+import Data.Type.Predicate
+import Data.Type.Predicate.Logic
+import Data.Type.Universe
 
 -- | A parameterized predicate.  See 'Found' for more information.
 type ParamPred k v = k -> Predicate v
@@ -72,6 +89,7 @@
 -- :: k@, we can prove or disprove the fact that there exists a @y :: v@
 -- such that @P x \@\@ y@.
 data Found :: ParamPred k v -> Predicate k
+
 type instance Apply (Found (p :: ParamPred k v)) a = Σ v (p a)
 
 -- | Convert a parameterized predicate into a predicate on the parameter.
@@ -97,11 +115,13 @@
 
 -- | Flip the arguments of a 'ParamPred'.
 data FlipPP :: ParamPred v k -> ParamPred k v
+
 type instance Apply (FlipPP p x) y = p y @@ x
 
 -- | Promote a @'Predicate' v@ to a @'ParamPred' k v@, ignoring the @k@
 -- input.
 data ConstPP :: Predicate v -> ParamPred k v
+
 type instance Apply (ConstPP p k) v = p @@ v
 
 -- | @Found ('EqBy' f) \@\@ x@ is true if there exists some value when,
@@ -116,6 +136,7 @@
 --
 -- @since 0.1.5.0
 data EqBy :: (v ~> k) -> ParamPred k v
+
 type instance Apply (EqBy f x) y = x :~: (f @@ y)
 
 -- | @Found ('IsTC' t) \@\@ x@ is true if @x@ was made using the unary type
@@ -158,29 +179,34 @@
 --
 -- @since 0.1.4.0
 data TyPP :: (k -> v -> Type) -> ParamPred k v
+
 type instance Apply (TyPP t k) v = t k v
 
 -- | Pre-compose a function to a 'ParamPred'.  Is essentially @'flip'
 -- ('.')@, but unfortunately defunctionalization doesn't work too well with
 -- that definition.
 data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v
+
 type instance Apply (PPMap f p x) y = p (f @@ x) @@ y
 
 -- | Pre-compose a function to a 'ParamPred', but on the "value" side.
 --
 -- @since 0.1.5.0
 data PPMapV :: (u ~> v) -> ParamPred k u -> ParamPred k v
+
 type instance Apply (PPMapV f p x) y = p x @@ (f @@ y)
 
 instance (Decidable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Decidable (Found (PPMap f p)) where
-    decide = mapDecision (\case i :&: p -> i :&: p)
-                         (\case i :&: p -> i :&: p)
-           . decide @(Found p)
-           . applySing (sing :: Sing f)     -- can just be sing @f in singletons 2.5, ghc 8.6+
+  decide =
+    mapDecision
+      (\case i :&: p -> i :&: p)
+      (\case i :&: p -> i :&: p)
+      . decide @(Found p)
+      . applySing (sing :: Sing f) -- can just be sing @f in singletons 2.5, ghc 8.6+
 
 instance (Provable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Provable (Found (PPMap f p)) where
-    prove (x :: Sing a) = case prove @(Found p) ((sing :: Sing f) @@ x) of
-        i :&: p -> i :&: p
+  prove (x :: Sing a) = case prove @(Found p) ((sing :: Sing f) @@ x) of
+    i :&: p -> i :&: p
 
 -- | A constraint that a @'ParamPred' k v@ is "searchable".  It means that
 -- for any input @x :: k@, we can prove or disprove that there exists a @y
@@ -191,7 +217,7 @@
 -- | A constraint that a @'ParamPred' k v@ s "selectable".  It means that
 -- for any input @x :: k@, we can always find a @y :: v@ that satisfies @P
 -- x \@\@ y@.  We can "select" that @y@, no matter what.
-type Selectable p = Provable  (Found p)
+type Selectable p = Provable (Found p)
 
 -- | The deciding/searching function for @'Searchable' p@.
 --
@@ -204,9 +230,10 @@
 --
 -- See 'searchTC' and 'SearchableTC' for a version that isn't ambiguously
 -- typed, but only works when @p@ is a type constructor.
-search
-    :: forall p. Searchable p
-    => Decide (Found p)
+search ::
+  forall p.
+  Searchable p =>
+  Decide (Found p)
 search = decide @(Found p)
 
 -- | The proving/selecting function for @'Selectable' p@.
@@ -220,9 +247,10 @@
 --
 -- See 'selectTC' and 'SelectableTC' for a version that isn't ambiguously
 -- typed, but only works when @p@ is a type constructor.
-select
-    :: forall p. Selectable p
-    => Prove (Found p)
+select ::
+  forall p.
+  Selectable p =>
+  Prove (Found p)
 select = prove @(Found p)
 
 -- | If @T :: k -> v -> 'Type'@ is a type constructor, then @'SearchableTC'
@@ -261,7 +289,7 @@
 -- TypeApplications to use.
 --
 -- @since 0.1.4.0
-type SelectableTC t = Provable  (Found (TyPP t))
+type SelectableTC t = Provable (Found (TyPP t))
 
 -- | The canonical selecting function for @'Searchable' t@.
 --
@@ -270,9 +298,10 @@
 -- can be inferred from the result type.
 --
 -- @since 0.1.4.0
-searchTC
-    :: forall t. SearchableTC t
-    => Decide (Found (TyPP t))
+searchTC ::
+  forall t.
+  SearchableTC t =>
+  Decide (Found (TyPP t))
 searchTC = search @(TyPP t)
 
 -- | The canonical selecting function for @'SelectableTC' t@.
@@ -282,9 +311,10 @@
 -- can be inferred from the result type.
 --
 -- @since 0.1.4.0
-selectTC
-    :: forall t. SelectableTC t
-    => Prove (Found (TyPP t))
+selectTC ::
+  forall t.
+  SelectableTC t =>
+  Prove (Found (TyPP t))
 selectTC = select @(TyPP t)
 
 -- | A @'ParamPred' (f k) k@.  Parameterized on an @as :: f k@, returns
@@ -306,17 +336,19 @@
 inPNotNull _ (s :&: i) = WitAny i s
 
 instance Universe f => Decidable (Found (InP f)) where
-    decide = mapDecision (\case WitAny i s -> s :&: i    )
-                         (\case s :&: i     -> WitAny i s)
-           . decide @(NotNull f)
+  decide =
+    mapDecision
+      (\case WitAny i s -> s :&: i)
+      (\case s :&: i -> WitAny i s)
+      . decide @(NotNull f)
 
 instance Decidable (NotNull f ==> Found (InP f))
 instance Provable (NotNull f ==> Found (InP f)) where
-    prove = notNullInP
+  prove = notNullInP
 
 instance Decidable (Found (InP f) ==> NotNull f)
 instance Provable (Found (InP f) ==> NotNull f) where
-    prove = inPNotNull
+  prove = inPNotNull
 
 -- | @'AnyMatch' f@ takes a parmaeterized predicate on @k@ (testing for
 -- a @v@) and turns it into a parameterized predicate on @f k@ (testing for
@@ -329,18 +361,22 @@
 -- A @'ParamPred' k v@ tests if a @k@ can create some @v@.  The resulting
 -- @'ParamPred' (f k) v@ tests if any @k@ in @f k@ can create some @v@.
 data AnyMatch f :: ParamPred k v -> ParamPred (f k) v
+
 type instance Apply (AnyMatch f p as) a = Any f (FlipPP p a) @@ as
 
 instance (Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p)) where
-    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))
+  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
@@ -348,27 +384,28 @@
 --
 -- @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)
+  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
+  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)
+  prove x = case select @p x of
+    s :&: p -> case select @q x of
+      t :&: q -> STuple2 s t :&: (p, q)
diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs
--- a/src/Data/Type/Predicate/Quantification.hs
+++ b/src/Data/Type/Predicate/Quantification.hs
@@ -1,10 +1,11 @@
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeInType          #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- |
 -- Module      : Data.Type.Predicate.Quantification
@@ -17,40 +18,66 @@
 --
 -- Higher-level predicates for quantifying predicates over universes and
 -- sets.
---
 module Data.Type.Predicate.Quantification (
   -- * Any
-    Any, WitAny(..), None, anyImpossible
+  Any,
+  WitAny (..),
+  None,
+  anyImpossible,
+
   -- ** Decision
-  , decideAny, idecideAny, decideNone, idecideNone
+  decideAny,
+  idecideAny,
+  decideNone,
+  idecideNone,
+
   -- ** Entailment
-  , entailAny, ientailAny, entailAnyF, ientailAnyF
+  entailAny,
+  ientailAny,
+  entailAnyF,
+  ientailAnyF,
+
   -- * All
-  , All, WitAll(..), NotAll
+  All,
+  WitAll (..),
+  NotAll,
+
   -- ** Decision
-  , decideAll, idecideAll
+  decideAll,
+  idecideAll,
+
   -- ** Entailment
-  , entailAll, ientailAll, entailAllF, ientailAllF
-  , decideEntailAll, idecideEntailAll
+  entailAll,
+  ientailAll,
+  entailAllF,
+  ientailAllF,
+  decideEntailAll,
+  idecideEntailAll,
+
   -- * Logical interplay
-  , allToAny
-  , allNotNone, noneAllNot
-  , anyNotNotAll, notAllAnyNot
-  ) where
+  allToAny,
+  allNotNone,
+  noneAllNot,
+  anyNotNotAll,
+  notAllAnyNot,
+) where
 
-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.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
 
 -- | 'decideNone', but providing an 'Elem'.
-idecideNone
-    :: forall f k (p :: k ~> Type) (as :: f k). Universe f
-    => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))    -- ^ predicate on value
-    -> (Sing as -> Decision (None f p @@ as))                    -- ^ predicate on collection
+idecideNone ::
+  forall f k (p :: k ~> Type) (as :: f k).
+  Universe f =>
+  -- | predicate on value
+  (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
+  -- | predicate on collection
+  (Sing as -> Decision (None f p @@ as))
 idecideNone f xs = decideNot @(Any f p) $ idecideAny f xs
 
 -- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
@@ -59,50 +86,61 @@
 --
 -- That is, it turns a predicate of kind @k ~> Type@ into a predicate
 -- of kind @f k ~> Type@.
-decideNone
-    :: forall f k (p :: k ~> Type). Universe f
-    => Decide p                         -- ^ predicate on value
-    -> Decide (None f p)                -- ^ predicate on collection
+decideNone ::
+  forall f k (p :: k ~> Type).
+  Universe f =>
+  -- | predicate on value
+  Decide p ->
+  -- | predicate on collection
+  Decide (None f p)
 decideNone f = idecideNone (const f)
 
 -- | 'entailAny', but providing an 'Elem'.
-ientailAny
-    :: forall f p q as. (Universe f, SingI as)
-    => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)        -- ^ implication
-    -> Any f p @@ as
-    -> Any f q @@ as
+ientailAny ::
+  forall f p q as.
+  (Universe f, SingI as) =>
+  -- | implication
+  (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) ->
+  Any f p @@ as ->
+  Any f q @@ as
 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@.
-entailAny
-    :: forall f p q. Universe f
-    => (p --> q)
-    -> (Any f p --> Any f q)
+entailAny ::
+  forall f p q.
+  Universe f =>
+  (p --> q) ->
+  (Any f p --> Any f q)
 entailAny = tmap @(Any f)
 
 -- | 'entailAll', but providing an 'Elem'.
-ientailAll
-    :: forall f p q as. (Universe f, SingI as)
-    => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)      -- ^ implication
-    -> All f p @@ as
-    -> All f q @@ as
+ientailAll ::
+  forall f p q as.
+  (Universe f, SingI as) =>
+  -- | implication
+  (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) ->
+  All f p @@ as ->
+  All f q @@ as
 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@.
-entailAll
-    :: forall f p q. Universe f
-    => (p --> q)
-    -> (All f p --> All f q)
+entailAll ::
+  forall f p q.
+  Universe f =>
+  (p --> q) ->
+  (All f p --> All f q)
 entailAll = tmap @(All f)
 
 -- | 'entailAnyF', but providing an 'Elem'.
-ientailAnyF
-    :: forall f p q as h. Functor h
-    => (forall a. Elem f as a -> p @@ a -> h (q @@ a))      -- ^ implication in context
-    -> Any f p @@ as
-    -> h (Any f q @@ as)
+ientailAnyF ::
+  forall f p q as h.
+  Functor h =>
+  -- | implication in context
+  (forall a. Elem f as a -> p @@ a -> h (q @@ a)) ->
+  Any f p @@ as ->
+  h (Any f q @@ as)
 ientailAnyF f = \case WitAny i x -> WitAny i <$> f i x
 
 -- | If @p@ implies @q@ under some context @h@, and if there exists some
@@ -116,46 +154,58 @@
 -- This is if the @p a -> 'Decision' (q a)@ implication is false, there
 -- it doesn't mean that there is /no/ @a@ such that @q a@, necessarily.
 -- There could have been an @a@ where @p@ does not hold, but @q@ does.
-entailAnyF
-    :: forall f p q h. (Universe f, Functor h)
-    => (p --># q) h                                     -- ^ implication in context
-    -> (Any f p --># Any f q) h
-entailAnyF f x a = withSingI x $
+entailAnyF ::
+  forall f p q h.
+  (Universe f, Functor h) =>
+  -- | implication in context
+  (p --># q) h ->
+  (Any f p --># Any f q) h
+entailAnyF f x a =
+  withSingI x $
     ientailAnyF @f @p @q (\i -> f (indexSing i x)) a
 
 -- | 'entailAllF', but providing an 'Elem'.
-ientailAllF
-    :: forall f p q as h. (Universe f, Applicative h, SingI as)
-    => (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 = fmap (prodAll getWit)
-                . itraverseProd (\i _ -> Wit @q <$> f i (runWitAll a i))
-                $ singProd (sing @as)
+ientailAllF ::
+  forall f p q as h.
+  (Universe f, Applicative h, SingI as) =>
+  -- | implication in context
+  (forall a. Elem f as a -> p @@ a -> h (q @@ a)) ->
+  All f p @@ as ->
+  h (All f q @@ as)
+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@.
-entailAllF
-    :: forall f p q h. (Universe f, Applicative h)
-    => (p --># q) h                                     -- ^ implication in context
-    -> (All f p --># All f q) h
-entailAllF f x a = withSingI x $
+entailAllF ::
+  forall f p q h.
+  (Universe f, Applicative h) =>
+  -- | implication in context
+  (p --># q) h ->
+  (All f p --># All f q) h
+entailAllF f x a =
+  withSingI x $
     ientailAllF @f @p @q (\i -> f (indexSing i x)) a
 
 -- | 'entailAllF', but providing an 'Elem'.
-idecideEntailAll
-    :: forall f p q as. (Universe f, SingI as)
-    => (forall a. Elem f as a -> p @@ a -> Decision (q @@ a))     -- ^ decidable implication
-    -> All f p @@ as
-    -> Decision (All f q @@ as)
+idecideEntailAll ::
+  forall f p q as.
+  (Universe f, SingI as) =>
+  -- | decidable implication
+  (forall a. Elem f as a -> p @@ a -> Decision (q @@ a)) ->
+  All f p @@ as ->
+  Decision (All f q @@ as)
 idecideEntailAll f a = idecideAll (\i _ -> f i (runWitAll a i)) sing
 
 -- | If we have @p a@ for all @a@, and @p a@ can be used to test for @q a@,
 -- then we can test all @a@s for @q a@.
-decideEntailAll
-    :: forall f p q. Universe f
-    => p -?> q
-    -> All f p -?> All f q
+decideEntailAll ::
+  forall f p q.
+  Universe f =>
+  p -?> q ->
+  All f p -?> All f q
 decideEntailAll = dmap @(All f)
 
 -- | It is impossible for any value in a collection to be 'Impossible'.
@@ -176,13 +226,14 @@
 -- order to locate that specific @a@.
 --
 -- @since 0.1.2.0
-notAllAnyNot
-    :: forall f p. (Universe f, Decidable p)
-    => NotAll f p --> Any f (Not p)
+notAllAnyNot ::
+  forall f p.
+  (Universe f, Decidable p) =>
+  NotAll f p --> Any f (Not p)
 notAllAnyNot xs vAll = elimDisproof (decide @(Any f (Not p)) xs) $ \vAny ->
-    vAll $ WitAll $ \i ->
-      elimDisproof (decide @p (indexSing i xs)) $ \vP ->
-        vAny $ WitAny i vP
+  vAll $ WitAll $ \i ->
+    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
 -- @p@.
@@ -195,11 +246,12 @@
 -- @as@.  Requires @'Decidable' p@ to interrogate the input disproof.
 --
 -- @since 0.1.2.0
-noneAllNot
-    :: forall f p. (Universe f, Decidable p)
-    => None f p --> All f (Not p)
+noneAllNot ::
+  forall f p.
+  (Universe f, Decidable p) =>
+  None f p --> All f (Not p)
 noneAllNot xs vAny = elimDisproof (decide @(All f (Not p)) xs) $ \vAll ->
-    vAll $ WitAll $ \i p -> vAny $ WitAny i p
+  vAll $ WitAll $ \i p -> vAny $ WitAny i p
 
 -- | If something is true for all xs, then it must be true for at least one
 -- x in xs, provided that xs is not empty.
diff --git a/src/Data/Type/Universe.hs b/src/Data/Type/Universe.hs
--- a/src/Data/Type/Universe.hs
+++ b/src/Data/Type/Universe.hs
@@ -1,21 +1,16 @@
-{-# 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 CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
-{-# LANGUAGE TypeInType             #-}
-{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- |
 -- Module      : Data.Type.Universe
@@ -28,47 +23,75 @@
 --
 -- A type family for "containers", intended for allowing lifting of
 -- predicates on @k@ to be predicates on containers @f k@.
---
 module Data.Type.Universe (
   -- * Universe
-    Elem, In, Universe(..)
-  , singAll
+  Elem,
+  In,
+  Universe (..),
+  singAll,
+
   -- ** Instances
-  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IIdentity(..)
+  Index (..),
+  IJust (..),
+  IRight (..),
+  NEIndex (..),
+  ISnd (..),
+  IIdentity (..),
+
   -- ** Predicates
-  , All, WitAll(..), NotAll
-  , Any, WitAny(..), None
-  , Null, NotNull
+  All,
+  WitAll (..),
+  NotAll,
+  Any,
+  WitAny (..),
+  None,
+  Null,
+  NotNull,
+
   -- *** Specialized
-  , IsJust, IsNothing, IsRight, IsLeft
+  IsJust,
+  IsNothing,
+  IsRight,
+  IsLeft,
+
   -- * Decisions and manipulations
-  , decideAny, decideAll
-  , genAll, igenAll
-  , splitSing
-  , pickElem
-  ) where
+  decideAny,
+  decideAll,
+  genAll,
+  igenAll,
+  splitSing,
+  pickElem,
+) where
 
-import           Data.Either.Singletons hiding    (IsLeft, IsRight)
-import           Data.Functor.Identity
-import           Data.Functor.Identity.Singletons
-import           Data.Kind
-import           Data.List.NonEmpty               (NonEmpty(..))
-import           Data.List.Singletons hiding      (Elem, ElemSym0, ElemSym1, ElemSym2, All, Any, Null)
-import           Data.Maybe.Singletons hiding     (IsJust, IsNothing)
-import           Data.Singletons
-import           Data.Singletons.Decide
-import           Data.Tuple.Singletons
-import           Data.Type.Functor.Product
-import           Data.Type.Predicate
-import           Data.Type.Predicate.Logic
-import           GHC.Generics                     ((:*:)(..))
-import           Prelude hiding                   (any, all)
-import qualified Data.List.NonEmpty.Singletons    as NE
+import Data.Either.Singletons hiding (IsLeft, IsRight)
+import Data.Functor.Identity
+import Data.Functor.Identity.Singletons
+import Data.Kind
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.List.NonEmpty.Singletons as NE
+import Data.List.Singletons hiding (
+  All,
+  Any,
+  Elem,
+  ElemSym0,
+  ElemSym1,
+  ElemSym2,
+  Null,
+ )
+import Data.Maybe.Singletons hiding (IsJust, IsNothing)
+import Data.Singletons
+import Data.Singletons.Decide
+import Data.Tuple.Singletons
+import Data.Type.Functor.Product
+import Data.Type.Predicate
+import Data.Type.Predicate.Logic
+import GHC.Generics ((:*:) (..))
+import Prelude hiding (all, any)
 
 -- | A @'WitAny' p as@ is a witness that, for at least one item @a@ in the
 -- type-level collection @as@, the predicate @p a@ is true.
 data WitAny f :: (k ~> Type) -> f k -> Type where
-    WitAny :: Elem f as a -> p @@ a -> WitAny f p as
+  WitAny :: Elem f as a -> p @@ a -> WitAny f p as
 
 -- | An @'Any' f p@ is a predicate testing a collection @as :: f a@ for the
 -- fact that at least one item in @as@ satisfies @p@.  Represents the
@@ -77,11 +100,12 @@
 -- This is mostly useful for its 'Decidable' and 'TFunctor' instances,
 -- which lets you lift predicates on @p@ to predicates on @'Any' f p@.
 data Any f :: Predicate k -> Predicate (f k)
+
 type instance Apply (Any f p) as = WitAny f p as
 
 -- | A @'WitAll' p as@ is a witness that the predicate @p a@ is true for all
 -- items @a@ in the type-level collection @as@.
-newtype WitAll f p (as :: f k) = WitAll { runWitAll :: forall a. Elem f as a -> p @@ a }
+newtype WitAll f p (as :: f k) = WitAll {runWitAll :: forall a. Elem f as a -> p @@ a}
 
 -- | An @'All' f p@ is a predicate testing a collection @as :: f a@ for the
 -- fact that /all/ items in @as@ satisfy @p@.  Represents the "forall"
@@ -91,60 +115,68 @@
 -- instances, which lets you lift predicates on @p@ to predicates on @'All'
 -- f p@.
 data All f :: Predicate k -> Predicate (f k)
+
 type instance Apply (All f p) as = WitAll f p as
 
 instance (Universe f, Decidable p) => Decidable (Any f p) where
-    decide = decideAny @f @_ @p $ decide @p
+  decide = decideAny @f @_ @p $ decide @p
 
 instance (Universe f, Decidable p) => Decidable (All f p) where
-    decide = decideAll @f @_ @p $ decide @p
+  decide = decideAll @f @_ @p $ decide @p
 
-instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p) where
+instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p)
 
 instance Provable p => Provable (NotNull f ==> Any f p) where
-    prove _ (WitAny i s) = WitAny i (prove @p s)
+  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 (indexSing 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 (indexSing 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 (indexSing 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
+  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 FProd f => Universe (f :: Type -> Type) where
-
-    -- | 'decideAny', but providing an 'Elem'.
-    idecideAny
-        :: forall k (p :: k ~> Type) (as :: f k). ()
-        => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value
-        -> (Sing as -> Decision (Any f p @@ as))                         -- ^ predicate on collection
+  -- | 'decideAny', but providing an 'Elem'.
+  idecideAny ::
+    forall k (p :: k ~> Type) (as :: f k).
+    () =>
+    -- | predicate on value
+    (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
+    -- | predicate on collection
+    (Sing as -> Decision (Any f p @@ as))
 
-    -- | 'decideAll', but providing an 'Elem'.
-    idecideAll
-        :: forall k (p :: k ~> Type) (as :: f k). ()
-        => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value
-        -> (Sing as -> Decision (All f p @@ as))                         -- ^ predicate on collection
+  -- | 'decideAll', but providing an 'Elem'.
+  idecideAll ::
+    forall k (p :: k ~> Type) (as :: f k).
+    () =>
+    -- | predicate on value
+    (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
+    -- | predicate on collection
+    (Sing as -> Decision (All f p @@ as))
 
-    allProd
-        :: forall p g. ()
-        => (forall a. Sing a -> p @@ a -> g a)
-        -> All f p --> TyPred (Prod f g)
+  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
+  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))
+type Null f = (None f Evident :: Predicate (f k))
 
 -- | Predicate that a given @as :: f k@ is not empty, and has at least one
 -- item in it.
@@ -166,10 +198,13 @@
 -- of kind @f k ~> Type@.
 --
 -- Essentially tests existential quantification.
-decideAny
-    :: forall f k (p :: k ~> Type). Universe f
-    => Decide p                                 -- ^ predicate on value
-    -> Decide (Any f p)                -- ^ predicate on collection
+decideAny ::
+  forall f k (p :: k ~> Type).
+  Universe f =>
+  -- | predicate on value
+  Decide p ->
+  -- | predicate on collection
+  Decide (Any f p)
 decideAny f = idecideAny (const f)
 
 -- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
@@ -180,59 +215,73 @@
 -- of kind @f k ~> Type@.
 --
 -- Essentially tests universal quantification.
-decideAll
-    :: forall f k (p :: k ~> Type). Universe f
-    => Decide p                                 -- ^ predicate on value
-    -> Decide (All f p)                -- ^ predicate on collection
+decideAll ::
+  forall f k (p :: k ~> Type).
+  Universe f =>
+  -- | predicate on value
+  Decide p ->
+  -- | predicate on collection
+  Decide (All f p)
 decideAll f = idecideAll (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 ::
+  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
+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 ::
+  forall f k (p :: k ~> Type) (as :: f k).
+  Universe f =>
+  -- | always-true predicate on value
+  (forall a. Elem f as a -> Sing a -> p @@ a) ->
+  -- | always-true predicate on collection
+  (Sing as -> All f p @@ as)
 igenAll 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'.
-genAll
-    :: 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 ::
+  forall f k (p :: k ~> Type).
+  Universe f =>
+  -- | always-true predicate on value
+  Prove p ->
+  -- | always-true predicate on collection
+  Prove (All f p)
 genAll f = prodAll f . singProd
 
 -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
-singAll
-    :: forall f k (as :: f k). Universe f
-    => Sing as
-    -> All f Evident @@ as
+singAll ::
+  forall f k (as :: f k).
+  Universe f =>
+  Sing as ->
+  All f Evident @@ as
 singAll = prodAll id . singProd
 
 -- | Test that a 'Maybe' is 'Just'.
 --
 -- @since 0.1.2.0
-type IsJust    = (NotNull Maybe :: Predicate (Maybe k))
+type IsJust = (NotNull Maybe :: Predicate (Maybe k))
 
 -- | Test that a 'Maybe' is 'Nothing'.
 --
 -- @since 0.1.2.0
-type IsNothing = (Null    Maybe :: Predicate (Maybe k))
+type IsNothing = (Null Maybe :: Predicate (Maybe k))
 
 -- | Test that an 'Either' is 'Right'
 --
@@ -242,168 +291,178 @@
 -- | Test that an 'Either' is 'Left'
 --
 -- @since 0.1.2.0
-type IsLeft  = (Null    (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 f = \case
-      SNil -> Disproved $ \case
-        WitAny i _ -> case i of {}
-      x `SCons` xs -> case f IZ x of
-        Proved p    -> Proved $ WitAny IZ p
-        Disproved v -> case idecideAny @[] @_ @p (f . IS) xs of
-          Proved (WitAny i p) -> Proved $ WitAny (IS i) p
-          Disproved vs -> Disproved $ \case
-            WitAny IZ     p -> v p
-            WitAny (IS i) p -> vs (WitAny i p)
+  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 f = \case
+    SNil -> Disproved $ \case
+      WitAny i _ -> case i of {}
+    x `SCons` xs -> case f IZ x of
+      Proved p -> Proved $ WitAny IZ p
+      Disproved v -> case idecideAny @[] @_ @p (f . IS) xs of
+        Proved (WitAny i p) -> Proved $ WitAny (IS i) p
+        Disproved vs -> Disproved $ \case
+          WitAny IZ p -> v p
+          WitAny (IS i) p -> vs (WitAny i 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 f = \case
-      SNil -> Proved $ WitAll $ \case {}
-      x `SCons` xs -> case f IZ x of
-        Proved p -> case idecideAll @[] @_ @p (f . IS) xs of
-          Proved a -> Proved $ WitAll $ \case
-            IZ   -> p
-            IS i -> runWitAll a i
-          Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)
-        Disproved v -> Disproved $ \a -> v $ runWitAll a IZ
+  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 f = \case
+    SNil -> Proved $ WitAll $ \case {}
+    x `SCons` xs -> case f IZ x of
+      Proved p -> case idecideAll @[] @_ @p (f . IS) xs of
+        Proved a -> Proved $ WitAll $ \case
+          IZ -> p
+          IS i -> runWitAll a i
+        Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)
+      Disproved v -> Disproved $ \a -> v $ runWitAll a IZ
 
-    allProd
-        :: forall p g. ()
-        => (forall a. Sing a -> p @@ a -> g a)
-        -> All [] p --> TyPred (Prod [] g)
-    allProd f = go
-      where
-        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))
+  allProd ::
+    forall p g.
+    () =>
+    (forall a. Sing a -> p @@ a -> g a) ->
+    All [] p --> TyPred (Prod [] g)
+  allProd f = go
+    where
+      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))
 
-    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
+  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
-      SNothing -> Disproved $ \case WitAny i _ -> case i of {}
-      SJust x  -> case f IJust x of
-        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
-    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
+  idecideAny f = \case
+    SNothing -> Disproved $ \case WitAny i _ -> case i of {}
+    SJust x -> case f IJust x of
+      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
+  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
-      SLeft  _ -> Disproved $ \case WitAny i _ -> case i of {}
-      SRight x -> case f IRight x of
-        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
-    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
+  idecideAny f = \case
+    SLeft _ -> Disproved $ \case WitAny i _ -> case i of {}
+    SRight x -> case f IRight x of
+      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
+  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
-        :: 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 f (x NE.:%| xs) = case f NEHead x of
-      Proved p    -> Proved $ WitAny NEHead p
-      Disproved v -> case idecideAny @[] @_ @p (f . NETail) xs of
-        Proved (WitAny i p) -> Proved $ WitAny (NETail i) p
-        Disproved vs     -> Disproved $ \case
-          WitAny i p -> case i of
-            NEHead    -> v p
-            NETail i' -> vs (WitAny i' p)
+  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 f (x NE.:%| xs) = case f NEHead x of
+    Proved p -> Proved $ WitAny NEHead p
+    Disproved v -> case idecideAny @[] @_ @p (f . NETail) xs of
+      Proved (WitAny i p) -> Proved $ WitAny (NETail i) p
+      Disproved vs -> Disproved $ \case
+        WitAny i p -> case i of
+          NEHead -> v p
+          NETail i' -> vs (WitAny i' 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 f (x NE.:%| xs) = case f NEHead x of
-      Proved p -> case idecideAll @[] @_ @p (f . NETail) xs of
-        Proved ps -> Proved $ WitAll $ \case
-          NEHead   -> p
-          NETail i -> runWitAll ps i
-        Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)
-      Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead
+  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 f (x NE.:%| xs) = case f NEHead x of
+    Proved p -> case idecideAll @[] @_ @p (f . NETail) xs of
+      Proved ps -> Proved $ WitAll $ \case
+        NEHead -> p
+        NETail i -> runWitAll ps i
+      Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)
+    Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead
 
-    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 ::
+    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
+  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
-    allProd f (STuple2 w x) a = PTup w $ f x (runWitAll a ISnd)
-    prodAll f (PTup _ x) = WitAll $ \case ISnd -> f x
+  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
+  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.
 instance Universe Identity where
-    idecideAny f (SIdentity x) =
-        mapDecision (WitAny IId)
-                    (\case WitAny IId p -> p)
+  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)
-                    (\y -> runWitAll y IId)
+  idecideAll f (SIdentity x) =
+    mapDecision
+      (\p -> WitAll $ \case IId -> p)
+      (\y -> runWitAll y IId)
       $ f IId x
-    allProd f (SIdentity x) a = PIdentity $ f x (runWitAll a IId)
-    prodAll f (PIdentity x) = WitAll $ \case IId -> f x
+  allProd f (SIdentity x) a = PIdentity $ f x (runWitAll a IId)
+  prodAll f (PIdentity x) = WitAll $ \case IId -> f x
diff --git a/src/Data/Type/Universe/Subset.hs b/src/Data/Type/Universe/Subset.hs
--- a/src/Data/Type/Universe/Subset.hs
+++ b/src/Data/Type/Universe/Subset.hs
@@ -1,10 +1,11 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeInType          #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- |
 -- Module      : Data.Type.Universe.Subset
@@ -16,72 +17,88 @@
 -- Portability : non-portable
 --
 -- Represent a decidable subset of a type-level collection.
---
 module Data.Type.Universe.Subset (
   -- * Subset
-    Subset, WitSubset(..)
-  , makeSubset
+  Subset,
+  WitSubset (..),
+  makeSubset,
+
   -- ** Subset manipulation
-  , intersection, union, symDiff, mergeSubset, imergeSubset
-  , mapSubset, imapSubset
+  intersection,
+  union,
+  symDiff,
+  mergeSubset,
+  imergeSubset,
+  mapSubset,
+  imapSubset,
+
   -- ** Subset extraction
-  , subsetToList
+  subsetToList,
+
   -- ** Subset tests
-  , subsetToAny, subsetToAll, subsetToNone
+  subsetToAny,
+  subsetToAll,
+  subsetToNone,
+
   -- ** Subset construction
-  , emptySubset, fullSubset
-  ) where
+  emptySubset,
+  fullSubset,
+) where
 
-import           Control.Applicative
-import           Data.Kind
-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
-import           Data.Type.Universe
+import Control.Applicative
+import Data.Kind
+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
+import Data.Type.Universe
 
 -- | A @'WitSubset' f p @@ as@ describes a /decidable/ subset of type-level
 -- collection @as@.
 newtype WitSubset f p (as :: f k) = WitSubset
-    { runWitSubset :: forall a. Elem f as a -> Decision (p @@ a)
-    }
+  { runWitSubset :: forall a. Elem f as a -> Decision (p @@ a)
+  }
 
 -- | A @'Subset' f p@ is a predicate that some decidable subset of an input
 -- @as@ is true.
 data Subset f :: (k ~> Type) -> (f k ~> Type)
+
 type instance Apply (Subset f p) as = WitSubset f p as
 
 instance (Universe f, Decidable p) => Decidable (Subset f p)
 instance (Universe f, Decidable p) => Provable (Subset f p) where
-    prove = makeSubset @f @_ @p (\_ -> decide @p)
+  prove = makeSubset @f @_ @p (\_ -> decide @p)
 
 -- | Create a 'Subset' from a predicate.
-makeSubset
-    :: forall f k p (as :: f k). Universe f
-    => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
-    -> Sing as
-    -> Subset f p @@ as
+makeSubset ::
+  forall f k p (as :: f k).
+  Universe f =>
+  (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
+  Sing as ->
+  Subset f p @@ as
 makeSubset f xs = WitSubset $ \i -> f i (indexSing i xs)
 
 -- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied
 -- predicates.
 --
 -- List is meant to include no duplicates.
-subsetToList
-    :: forall f p t. (Universe f, Alternative t)
-    => (Subset f p --># Any f p) t
+subsetToList ::
+  forall f p t.
+  (Universe f, Alternative t) =>
+  (Subset f p --># Any f p) t
 subsetToList xs s = getAlt $ (`ifoldMapSing` xs) $ \i _ -> Alt $ case runWitSubset s i of
-    Proved p    -> pure $ WitAny i p
-    Disproved _ -> empty
+  Proved p -> pure $ WitAny i p
+  Disproved _ -> empty
 
 -- | Restrict a 'Subset' to a single (arbitrary) member, or fail if none
 -- exists.
-subsetToAny
-    :: forall f p. Universe f
-    => Subset f p -?> Any f p
+subsetToAny ::
+  forall f p.
+  Universe f =>
+  Subset f p -?> Any f p
 subsetToAny xs s = idecideAny (\i _ -> runWitSubset s i) xs
 
 -- | Construct an empty subset.
@@ -97,67 +114,75 @@
 subsetToNone xs s = idecideNone (\i _ -> runWitSubset s i) xs
 
 -- | Combine two subsets based on a decision function
-imergeSubset
-    :: forall f k p q r (as :: f k). ()
-    => (forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-    -> Subset f p @@ as
-    -> Subset f q @@ as
-    -> Subset f r @@ as
+imergeSubset ::
+  forall f k p q r (as :: f k).
+  () =>
+  (forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) ->
+  Subset f p @@ as ->
+  Subset f q @@ as ->
+  Subset f r @@ as
 imergeSubset f ps qs = WitSubset $ \i ->
-    f i (runWitSubset ps i) (runWitSubset qs i)
+  f i (runWitSubset ps i) (runWitSubset qs i)
 
 -- | Combine two subsets based on a decision function
-mergeSubset
-    :: forall f k p q r (as :: f k). ()
-    => (forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-    -> Subset f p @@ as
-    -> Subset f q @@ as
-    -> Subset f r @@ as
+mergeSubset ::
+  forall f k p q r (as :: f k).
+  () =>
+  (forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) ->
+  Subset f p @@ as ->
+  Subset f q @@ as ->
+  Subset f r @@ as
 mergeSubset f = imergeSubset (\(_ :: Elem f as a) p -> f @a p)
 
 -- | Subset intersection
-intersection
-    :: forall f p q. ()
-    => ((Subset f p &&& Subset f q) --> Subset f (p &&& q))
+intersection ::
+  forall f p q.
+  () =>
+  ((Subset f p &&& Subset f q) --> Subset f (p &&& q))
 intersection _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideAnd @p @q @a
 
 -- | Subset union (left-biased)
-union
-    :: forall f p q. ()
-    => ((Subset f p &&& Subset f q) --> Subset f (p ||| q))
+union ::
+  forall f p q.
+  () =>
+  ((Subset f p &&& Subset f q) --> Subset f (p ||| q))
 union _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideOr @p @q @a
 
 -- | Symmetric subset difference
-symDiff
-    :: forall f p q. ()
-    => ((Subset f p &&& Subset f q) --> Subset f (p ^^^ q))
+symDiff ::
+  forall f p q.
+  () =>
+  ((Subset f p &&& Subset f q) --> Subset f (p ^^^ q))
 symDiff _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideXor @p @q @a
 
 -- | Test if a subset is equal to the entire original collection
-subsetToAll
-    :: forall f p. Universe f
-    => Subset f p -?> All f p
+subsetToAll ::
+  forall f p.
+  Universe f =>
+  Subset f p -?> All f p
 subsetToAll xs s = idecideAll (\i _ -> runWitSubset s i) xs
 
 -- | 'mapSubset', but providing an 'Elem'.
-imapSubset
-    :: (forall a. Elem f as a -> p @@ a -> q @@ a)
-    -> (forall a. Elem f as a -> q @@ a -> p @@ a)
-    -> Subset f p @@ as
-    -> Subset f q @@ as
+imapSubset ::
+  (forall a. Elem f as a -> p @@ a -> q @@ a) ->
+  (forall a. Elem f as a -> q @@ a -> p @@ a) ->
+  Subset f p @@ as ->
+  Subset f q @@ as
 imapSubset f g s = WitSubset $ \i ->
-    mapDecision (f i) (g i) (runWitSubset s i)
+  mapDecision (f i) (g i) (runWitSubset s i)
 
 -- | Map a bidirectional implication over a subset described by that
 -- implication.
 --
 -- Implication needs to be bidirectional, or otherwise we can't produce
 -- a /decidable/ subset as a result.
-mapSubset
-    :: Universe f
-    => (p --> q)
-    -> (q --> p)
-    -> (Subset f p --> Subset f q)
-mapSubset f g xs = withSingI xs $
-    imapSubset (\i -> f (indexSing i xs))
-               (\i -> g (indexSing i xs))
+mapSubset ::
+  Universe f =>
+  (p --> q) ->
+  (q --> p) ->
+  (Subset f p --> Subset f q)
+mapSubset f g xs =
+  withSingI xs $
+    imapSubset
+      (\i -> f (indexSing i xs))
+      (\i -> g (indexSing i xs))